1

我有一个项目在我的脑海中，我很好奇以前是否做过类似的事情。假设有一组不同类型的约束并且这些约束不能一起满足。

C = {c1, c2, c3, ..., cn}

(c1 and c2 and c3 ... cn) : 不能满足

我的目标是将这个集合分成 k 个集合（可能 k 非常小），以使每组约束都可以单独满足。

基本的解决方案是使用贪婪的方法。将选择一个约束作为第一个约束并标记为第一组。然后，将选择第二个并检查它是否可以用第一个约束解决。如果它们是可解的，那么第二个约束也将在第一组中，否则，它将被标记为第二组。这个过程将以这种方式继续，直到集合中没有任何约束。这样做的另一种方法可能是将约束分为 2 组，并检查这些组是否可以单独解决。如果不是，继续递归除法。这两种方法都受到大小的影响，它们将约束集划分为非常小的集合。

我正在寻找一种将约束集划分为 k 集的有效方法，其中 k 接近最优值（最小 k 值）。这里有 2 个挑战，1）可扩展性问题和 2）事先不知道约束结构。

4

1 回答 1

1

一个可以做你想做的事情的算法可以用经过充分研究的最小不可满足子集来表示。据我所知，这是他们最新的 SAT 竞赛曲目：http ://www.cril.univ-artois.fr/SAT11/results/results.php?idev=48

使用这个，下面的伪代码应该做你想要的

def sat_partition(CNF):
    partitions = {}
    while CNF is not empty:
        MUS = compute_mus(CNF)
        Remove one arbitrary element of MUS
        partitions += {MUS}
        CNF -= MUS
    return partitions
于 2015-10-27T03:08:50.490 回答