z3 - SATソルバーとしてZ3を使用したZ3極性

Question

Z3を使用して12000以上のブール変数でSAT問題を解決しようとしています。ソリューションでは、ほとんどの変数がfalseと評価されると思います。最初に「極性偽」を試すために、SATソルバーとしてZ3をガイドまたはヒントする方法はありますか？cryptominisat 2で試してみたところ、良い結果が得られました。

Answer 1

Z3は、ソルバーとプリプロセッサーのコレクションです。一部のソルバーにヒントを提供できます。コマンド(check-sat)を使用すると、Z3がソルバーを自動的に選択します。ソルバーを(check-sat-using <strategy>)自分で選択したい場合は、そうする必要があります。たとえば、次のコマンドは、ブールSATソルバーを使用するようにZ3に指示します。

(check-sat-using sat)

次を使用して、常に最初に「極性false」を試行するように強制できます。

(check-sat-using (with sat :phase always-false))

前処理ステップを制御することもできます。呼び出す前に数式をCNFに入れたい場合はsat、次を使用する必要があります。

(check-sat-using (then tseitin-cnf (with sat :phase always-false)))

編集：DIMACS入力形式とZ3 v4.3.1を使用している場合、コマンドラインを使用して使用可能なすべてのソルバーのパラメーターを設定することはできません。次のリリースでは、この制限に対処します。それまでの間、次を使用して進行中のブランチをダウンロードできます。

git clone https://git01.codeplex.com/z3 -b unstable 

Z3をコンパイルします。次に、極性をfalseに強制するには、コマンドラインオプションを使用します

sat.phase=always_false

このコマンドz3 -pm:satは、このモジュールで使用可能なすべてのオプションを表示します。

編集終了

SMT 2.0の完全な例を次に示します（オンラインでも入手可能）。

(declare-const p Bool)
(declare-const q Bool)
(declare-const r Bool)
(declare-const s Bool)

(assert (or (not p) (not q) (not r)))
(assert (or r s))
(assert (or r (not s)))
(assert (or r (and p q)))

(echo "With always false")
(check-sat-using (then tseitin-cnf (with sat :phase always-false)))
(get-model)
(echo "With always true")
(check-sat-using (then tseitin-cnf (with sat :phase always-true)))
(get-model)