satisfiability - SAT ソルバーを使用してすべての解を見つけることができますか?

Question

非常に興味深い質問だと思ったものへの回答を書きましたが、残念ながら、投稿する前にその質問は作成者によって削除されました。他の人に役立つ可能性がある場合に備えて、質問の要約と回答をここに再投稿します。

結合正規形のブール式が与えられると、解 (式を満たす変数割り当て) または問題が満たされないという情報を返す SAT ソルバーがあるとします。

このソルバーを使用してすべての解を見つけることはできますか?

Answer 1

あなたが説明した SAT ソルバーを使用して SAT 問題のすべての解を見つける方法は間違いなくありますが、それは最も効率的な方法ではないかもしれません。

ソルバーを使用して元の問題の解決策を見つけ、見つけたばかりの解決策を除外する以外に何もしない句を追加し、ソルバーを使用して新しい問題の解決策を見つける、などです。満足できない問題が発生するまで続けます。

---

たとえば、 を満たしたいとします(X or Y) and (X or Z)。次の 5 つの解決策があります。

• Xtrue の4 つ、YおよびZ任意。

• X偽YとZ真の1 つ。

ソルバーを実行すると、解が得られるとしましょう(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 ソルバーが解を探しているとき、問題について多くのことを学習しますが、すべての情報を返すわけではなく、見つけた解を返すだけです。ソルバーを再度実行すると、破棄されたすべての情報を再学習する必要があります。