Z3 Z3をSATソルバーとして使用する極性

Question

Z3を使用して12000+ブール変数でSAT問題を解決しようとしています。 私は、ほとんどの変数が解決策ではfalseと評価されると考えています。 SATソルバとしてZ3をガイドしたり、ヒントしたりする方法がありますか？ 私はcryptominisat 2でそれを試して、良い結果を得ました。

Answer 1

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

(check-sat-using sat) 

我々は常に使用して最初の「偽の極性」を試すためにそれを強制することができます。

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

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

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

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

をダウンロードし、Z3をコンパイルします。その後、極性偽を強制するために、我々は、このモジュールで使用可能なすべてのオプションを表示するコマンドラインオプション

sat.phase=always_false 

コマンドz3 -pm:satを使用します。

のEND EDITここ

は（onlineも利用可能）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)