optimization - minisat すべての SAT ソリューションを効率的に見つける方法

Question

このリンクで説明されている方法を使用して、すべてのソリューションを見つける方法を見つけました。

これは正常に動作していますが、遅いです。最初から制約を再計算するため、i_e は以前の計算を利用しません。

さて、この リンクで、MiniSat をライブラリとして使用してすべての解を見つけるより効率的な方法があることを確認しました。しかし、その方法はそこには記載されていません。

すべての SAT ソリューションを効率的に見つけるための適切なドキュメントを教えてください。

ありがとう。

Answer 1

すべての SAT 解を見つけるより効率的な方法は、Yu、Subramanyan、Tsiskaridze、および Malik による論文 ( "All-SAT using Minimal Blocking Clauses" ) で説明されています。

解決策を繰り返し見つけてブロッキング節を追加するという基本的な戦略は同じですが、ブロッキング節は斬新なアイデアを使用して生成され、サイズが縮小されます。生成されたブロッキング節は、通常の単純な部分代入よりも小さいため、反復ごとにより満足のいく代入が含まれ、列挙プロセスが高速化されます。

私の知る限り、ダウンロードして実行できる、このホワイト ペーパーに含まれるアイデアの公開された実装はありません。