1

Z3 を使用して、それぞれ 22 個の入力を持つ数百の XOR 句を含む充足可能性の問題を解決しています。XOR 句を DIMACS 形式でコーディングするために、Tseitin エンコーディングを使用しています。私の変換では、XOR をそれぞれ最大 5 つのリテラルを持つ小さな CNF 句に分割します。これまでのところ、Z3 は SAT ソリューションを考案できていません。

エンコーディングを改善するにはどうすればよいですか?

ガウスの消去法を見てきましたが、XOR 式には同じ入力変数がないため、これはおそらく役に立ちません。

4

1 に答える 1

2

Z3 には 2 つの SAT ソルバー エンジンがあり、戦略フレームワークを使用してより効率的なエンジンを有効にすることができます。たとえば、チュートリアルZ3 - 戦略を参照してください。

ビットベクトル式の戦略の使用を示すセクションがあります。

 (declare-const x (_ BitVec 16))
 (declare-const y (_ BitVec 16))
 (assert (= (bvor x y) (_ bv13 16)))
 (assert (bvslt x y))
 (check-sat-using (then simplify solve-eqs bit-blast sat))
 (get-model)

とはいえ、XOR を使用して CDCL ベースの SAT ソルバーのハード インスタンスを生成するのは比較的簡単です。例えば：

Randal E. Bryant: A View from the Engine Room: Computational Support for Symbolic Model Checking. 25 Years of Model Checking 2008: 145-149

Z3 のより効率的な sat ソルバー (上記の例で呼び出されます) には、xor (同等性) を検出して伝播するためのデータ構造がいくつかあります。

于 2013-01-20T01:09:09.473 に答える