我写了一个我认为是quite interesting question的答案，但不幸的是，该问题已被作者删除，然后才能发布。我在此重新发布问题和答案的摘要，以防其他人使用。
假设我有一个SAT解算器，给定正态形式的布尔公式，它返回一个解决方案（一个满足该公式的变量赋值）或该问题无法满足的信息。
我可以使用该求解器找到所有解决方案吗？
最佳答案
绝对有一种方法可以使用您描述的SAT解算器来找到SAT问题的所有解决方案，尽管这可能不是最有效的方法。
只需使用求解器找到您原来的问题的解决方案，添加一个除了排除您刚刚找到的解决方案之外什么都不做的子句，使用求解器找到新问题的解决方案，依此类推。继续努力直到遇到无法解决的问题。
例如，假设您要满足(X or Y) and (X or Z)。有五种解决方案：
四个X为true，Y和Z为任意。X为false，Y和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求解器正在寻找解决方案时，它会学到很多有关该问题的信息，但它不会将所有信息返回给您-它只是为您提供找到的解决方案。当您再次运行求解器时，它必须重新学习所有丢弃的信息。