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

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

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

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

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

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

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

来源

2015-10-20 genclik27

为什么你到底要做到这一点呢？如果您正在寻找调试方法，“不可核心”（或OR的Irreducable Inconsistent Subsystem）概念似乎密切相关。它在很多方面是相反的 - 一小部分不受约束的约束，从而消除其中的任何一个使得问题可以满足。你当然可以使用这些现有的算法来启发式地计算你想要的。 – tobyodavies

一个可以做你想做的算法可以用很少被研究的不可满足的子集来表示。这是最新的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-27 03:08:50 tobyodavies

Thansk的答案。我也发现了一种类似的方法http://ijcai.org/papers13/Papers/IJCAI13-098.pdf我将实现你的算法并让你知道结果。 – genclik27

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

回答

相关问题