2012-12-17 14 views
6

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

+0

は、スタックオーバーフローへようこそ!何を試しましたか? – IronMan84

+1

私はいくつかのCNF/DIMACSファイルを生成しています。 Z3/DIMACSですぐに解決できるものもあります。他の人は時間がかかったり、まったく終わらない。私はファイルにCryptominisat 2を使用し、 "--polarity-mode = false"を追加して解決しました。 Z3のINIパラメータでは、私は極性関連のパラメータを見つけることができませんでした。したがって、私はここでいくつかの賢明なヒントを見つけることを望んでいるstackoverflow。 –

答えて

5

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) 
+0

すぐにお返事ありがとうございます! –

+0

現在、私はZ3の入力フォーマットとしてDIMACSを使用しています。ヒントを活用するために、DIMACS/CNF句をSMT形式に翻訳する必要がありますか?私はZ3にブール式のSMTセットとして公式化された私の元の問題を解決させようとしました。しかし私は、SATソルバーが私の場合にはるかに高速であることを発見しました。 –

+0

私はDIMACS入力フォーマットに関連する情報で答えを更新しました。 –

関連する問題