10

を使用して大きなCNF 式を解こうとしていSAT solverます。数式 ( DIMACS形式) には4,697,898,048 = 2^32 + 402,930,752句があり、私が見つけたすべての SAT ソルバーで問題が発生しています。

  • (P)lingelingは、「節が多すぎる」(つまり、ヘッダー行が指定するよりも多くの節がありますが、そうではありません) があることを報告します。
  • CryptoMiniSat4とpicosatは、2^32 が少なすぎる 402,930,752 句とヘッダー行を読み取ると主張しています。
  • Glucoseは 98,916,961 節を解析し、単純化を使用して UNSAT として式を解いたと報告しているようですが、これが正しいとは考えられません (この短い式の最初のセグメントは SAT である可能性が非常に高いです)。

このサイズのファイルを処理できる SAT ソルバーを知っている人はいますか? または、この種の動作を回避できるコンパイラ スイッチのようなものはありますか? すべてのソルバーは64 ビット Linux用にコンパイルされていると思います。(これほど大きな数字を扱うのはちょっと初心者です、すみません。)

4

1 に答える 1

6

私は CryptoMiniSat の開発者です。CNF が非常に巨大なほとんどの場合、問題は SAT ソルバーではなく、元の問題から CNF への変換が十分に慎重に行われていないことにあります。その CNF を手で書いたのではなく、自動化されたツールを使用して CNF に変換した問題があったと思います。

問題を CNF に変換する行為はエンコーディングと呼ばれ、学界には膨大な文献があります。それ自体がトピック全体、またはより適切には、トピック全体がトピック全体です。Constraint Programming (CP)、Pseudo-boolean constraint (PB)、ANF から CNF への変換技術 (crypo ワークショップ/会議を参照)、および電子回路エンコーディング (AIG、Tseitin エンコーディングとそのバリアントを検索して見てください) に関する研究論文を参照してください。参照で）。これらは大きなトピックですが、他にもたくさんあります。これらをのぞいてみると、CNF が少なくとも 3 桁、おそらくそれ以上減少します。

于 2015-09-17T20:21:22.953 に答える