将不可满足的约束集合转换为可满足的较小约束集合

Question

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

C = {C1，C2，C3，...，CN}

（c1和c2和c3 ... CN）：不符合要求

我的目标是分割该组分为k集合（可能k非常小），使得每一组约束都可单独满足。

基本的解决方案是使用贪婪的方法。约束将被选作第一个约束并标记为第一组。然后，将选择第二个，并检查它是否可用第一个约束解决。如果它们是可解的，那么第二个约束也将在第一个组中，否则，它将被标记为第二个组。该过程将以这种方式继续，直到该集合中没有约束。做这件事的另一种方法可能是将约束分成两组，并检查这些组是否可以单独解决。如果不是，则继续递归分割。这两种方法的规模都很大，它们将约束条件分成很小的集合。

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

Answer 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