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

【问题标题】：Converting unsatisfiable set of constraints into satisfiable smaller sets of constraints将不可满足的约束集转换为可满足的较小约束集
【发布时间】：2015-10-20 14:11:47
【问题描述】：

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

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

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

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

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

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

【问题讨论】：

您究竟为什么要这样做？如果您正在寻找一种调试方法，“unsat core”（或来自 OR 的 Irreducable Inconsistent Subsystem）的概念似乎密切相关。它在许多方面是相反的——一个小的未满足的约束子集，这样删除它们中的任何一个都会使问题得到满足。你当然可以使用这些现有的算法来启发式地计算你想要的。

标签： constraint-programming satisfiability sat

【解决方案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

【讨论】：

感谢您的回答。我也找到了类似的方法ijcai.org/papers13/Papers/IJCAI13-098.pdf我会实现你的算法，让你知道结果。