是否可以使用SAT求解器查找所有解决方案？

我写了一个我认为是quite interesting question的答案，但不幸的是，这个问题在我发布之前被作者删除了。我在这里重新发布这个问题的总结和我的答案，以防其他人使用它。是否可以使用SAT求解器查找所有解决方案？

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

我可以用这个求解器找到全部是的解决方案吗？

2012-09-03 Vectornaut

谁downvoted请人能解释为什么？在阅读这篇博客文章（http://blog.stackoverflow.com/2011/07/its-ok-to-ask-and-answer-your-own-questions/）之后，我想我在这里做的是“不仅仅是好的“，但”明确鼓励“。 – Vectornaut

这很完美。很好的答案，顺便说一句。 –

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

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

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

四连X真实，Y和Z随心所欲。
One with X false，Y and Z true。

所以你运行你的解算器，并假设它为您提供了解决方案(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求解器正在寻找解决方案时，它会学习很多有关该问题的知识，但它不会将所有信息都返回给您 - 它只是为您提供找到的解决方案。当你再次运行求解器时，它必须重新学习所有扔掉的信息。

来源

2012-09-03 18:40:49 Vectornaut

当然可以。当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++接口执行此操作要快得多它可以保存中间数据，迭代速度会更快。

[1] http://minisat.se/

[2] http://fairmut3x.wordpress.com/2011/07/29/cnf-conjunctive-normal-form-dimacs-format-explained/

来源

2013-05-09 13:37:41

是否可以使用SAT求解器查找所有解决方案？

回答

相关问题