可以使用SAT求解器找到所有解决方案吗？

Question

我写了一个我认为是一个非常有趣的问题的答案,但不幸的是,在我发帖之前,这个问题被其作者删除了.我正在重新发布问题的摘要和我的答案,以防它可能对其他人有用.

假设我有一个SAT求解器,给定一个联合正规形式的布尔公式,返回一个解决方案(满足公式的变量赋值)或问题不可满足的信息.

我可以使用此求解器找到所有解决方案吗？

Answer 1

绝对有一种方法可以使用您描述的SAT求解器来找到SAT问题的所有解决方案,尽管它可能不是最有效的方法.

只需使用求解器找到原始问题的解决方案,添加一个除了排除刚刚找到的解决方案之外什么都不做的子句,使用求解器找到新问题的解决方案,等等.继续前进,直到遇到不可满足的问题.

例如,假设您想要满足(X or Y) and (X or Z).有五种解决方案:

所以你运行你的求解器,让我们说它给你解决方案(X, Y, Z) = (T, F, F).您可以使用约束排除此解决方案---并且只有此解决方案

not (X and (not Y) and (not Z))

可以将此约束重写为子句

(not X) or Y or Z

所以现在你可以在新问题上运行求解器了

(X or Y) and (X or Z) and ((not X) or Y or Z)

等等.

就像我说的,这是一种做你想要的方式,但它可能不是最有效的方式.当您的SAT求解器正在寻找解决方案时,它会对该问题有很多了解,但它不会将所有这些信息返回给您 - 它只是为您提供了找到的解决方案.当您再次运行解算器时,它必须重新学习丢弃的所有信息.

Answer 2

当然可以.当MiniSat [1]找到解决方案时

s SATISFIABLE
v 1 2 -3 0

(解决方案1 = True,2 = True,3 = False)那么你必须在原始CNF [2]中加入一个禁止这个解决方案的条款:

-1 -2 3 0

(这意味着,必须是1或2必须是False3 或2 True).然后你再次解决.你这样做直到求解器返回UNSAT,即没有更多的问题解决方案.您将插入一个子句每次迭代,每个条款都会有相同的格式解决方案不同的是这一切都倒并具有0在年底

使用MiniSat的C++接口来实现这一点要快得多,因为它可以保存中间数据并且迭代会更快.