satisfiability - SAT求解器可以用来找到所有的解决方案吗？

Question

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

假设我有一个 SAT 求解器，给定一个联合范式的布尔公式，它返回一个解（满足公式的变量赋值）或问题不可满足的信息。

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

score 11 · Accepted Answer

绝对有一种方法可以使用您描述的 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 求解器正在寻找解决方案时，它会了解很多关于该问题的信息，但它不会将所有这些信息返回给您——它只会为您提供它找到的解决方案。当您再次运行求解器时，它必须重新学习所有被丢弃的信息。

score 10 · Accepted Answer

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

s SATISFIABLE
v 1 2 -3 0

（解决方案 1= True, 2= True, 3= False）然后您必须在原始 CNF[2] 中添加一个禁止此解决方案的子句：

-1 -2 3 0

（这意味着 1 或 2 必须是False或 3 必须是True）。那你再解决。你这样做直到求解器返回UNSAT，即没有更多的解决方案。您将为每次迭代插入一个子句，每个子句将具有与解决方案相同的格式，除了它全部倒置并且0末尾有一个

使用 MiniSat 的 C++ 接口执行此操作要快得多，因为它可以保存中间数据并且迭代会更快。

2 回答 2