私はquite interesting questionだと思った答えを書いたが、不幸にも質問を投稿者が削除する前に投稿した。私は質問の要約と私の答えをここに再掲載しています。それが他の誰にとっても役に立つかもしれない場合に備えて。SATソルバーを使用してすべてのソリューションを見つけることはできますか？
結合標準形でブール式を指定すると、解（式を満たす変数の代入）または問題が満たされないという情報が返されるSATソルバーがあるとします。
このソルバーを使用してを見つけることはできますか？すべてソリューションですか？
あなたが説明したSATソルバーを使用して、SAT問題のすべての解決策を見つける方法は間違いありませんが、最も効率的な方法ではないかもしれません。
ソルバーを使用して元の問題の解を見つけ、見つかったばかりの解を除外するだけの句を追加したり、ソルバーを使用して新しい問題の解決策を見つけるなどしてください。満足できない問題が生じるまで続けてください。例えば
、あなたが(X or Y) and (X or Z)を満足するとします。真X、YとZ任意で
4：5つのソリューションがあります。
Xが1であり、YおよびZが真です。
ソルバーを実行して、解答(X, Y, Z) = (T, F, F)が得られたとしましょう。あなたはこの制約は、句ので
(not X) or Y or Z
今あなたがあなたのソルバーを実行できるように書き換えることができ制約
not (X and (not Y) and (not Z))
と---このソリューション---とだけこのソリューションを排除することができます新しい問題
(X or Y) and (X or Z) and ((not X) or Y or Z)
などです。
私が言ったように、これはあなたがしたいことをする方法ですが、おそらく最も効率的な方法ではありません。 SATソルバーが解決策を探しているとき、問題について多くのことを学んでいますが、すべての情報が返されるわけではありません。ソルバを再度実行すると、捨てられたすべての情報を再学習する必要があります。
確かに可能です。MiniSATは、[1]解決策を見つけると
s SATISFIABLE
v 1 2 -3 0
（溶液= True 1、= True 2、3 = False）、あなたはこのソリューションを禁止し、元のCNF [2]句に入れる必要があります：
-1 -2 3 0
（つまり、1または2のいずれかがFalseまたは3がTrueである必要があります）。その後、あなたは再び解決する。これは、ソルバーがUNSATを返すまで、つまり問題の解決策がもうなくなるまで実行されます。反復ごとに1つの句を挿入し、すべての句が反転され、末尾に0があることを除いて、同じ句が挿入されます。
これは、MiniSatのC++インターフェイスを使用する方がはるかに高速です。中間データを保存することができ、反復処理が高速になります。
[2] http://fairmut3x.wordpress.com/2011/07/29/cnf-conjunctive-normal-form-dimacs-format-explained/
くださいdownvoted人は理由を説明することはできますか？このブログのエントリー（http://blog.stackoverflow.com/2011/07/its-ok-to-ask-and-answer-your-own-questions/）を読んだ後、私はここで「単にOK "と答えたが、"明示的に奨励した。 – Vectornaut
これは大丈夫です。良い答え、btw。 –