satisfiability - 可以使用 SAT 求解器找到所有解吗？

Question

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

假设我有一个 SAT 求解器，给定一个合取范式的 bool 公式，它返回一个解决方案(满足公式的变量赋值)或问题不可满足的信息。

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

Answer 1

肯定有一种方法可以使用您描述的 SAT 求解器来查找 SAT 问题的所有解决方案，尽管它可能不是最有效的方法。

只需使用求解器找到原始问题的解决方案，添加一个除了排除刚刚找到的解决方案之外什么都不做的子句，使用求解器找到新问题的解决方案，等等。继续下去，直到遇到无法解决的问题。

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

四连X是的，Y和 Z随意的。

一带X假，Y和 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 求解器正在寻找解决方案时，它会了解很多有关问题的知识，但它不会将所有信息返回给您——它只是为您提供它找到的解决方案。当您再次运行求解器时，它必须重新学习所有被丢弃的信息。