簡単な問題。mxn マトリックスを表す非常に大きな CNF ファイルがあります。関連する用語を含む >10000 変数としましょう。したがって、最初のステップとして、CNF ファイルを分割するか、並列解決の概念のために行列を 100 の変数に分割することをお勧めします。どのルールを適用するかについての説明はありますか?
すべての助けに感謝します。
エイドリアンよろしく
1 に答える
1
Metisのようなグラフ分割ツールを使用して、変数を共有しない独立したセットに句をクラスター化できます。CNF
本当に切断されたクラスターを識別することができない場合、「リンク変数」の数はそれらの値を列挙するのに十分小さい可能性があります。このような列挙は、基本的に接続変数に暫定的な値を割り当て、検索プロセスから除外します。代償として、値の組み合わせごとに検索を実行する必要があります。
Cryptominisat 、 Riss3g、Lingelingなどの最新のSAT ソルバーは、問題のサイズを小さくするためにさまざまな前処理手段を適用します。ただし、10000 個の変数は、追加の手順なしで解決できる実行可能なサイズである可能性があります。
CNF サイズだけでは、信頼できる指標や問題の複雑さにはなりません。Tseitin エンコーディングは、CNF の節の数を減らすために頻繁に使用される手法です。
この投稿で推奨されているように: SAT エンコーディングに関して作業するための多くの有用なリファレンスを含む優れた論文は、Magnus Björk による「Successful SAT Encoding Techniques」、2009 年 7 月 25 日: http://jsat.ewi.tudelft.nl/addendum/です。 Bjork_encoding.pdf </p>
于 2014-04-08T09:06:48.803 に答える