0

ViZ3 を使用して、変数に対するブール制約と次の形式の制約で構成されるシステムを解決しています。

L < If(V0, T0, F0) + If(V1, T1, F1) + ... + If(Vn, Tn, Fn) <= H

ここLで、H、 、TiおよびFiは整数定数です。

すべての変数はブール値ですが、QF_LIA ソルバーは一般的なものよりも多少高速であることがわかったので、前者を使用しています。私の推測では、Z3 は新しい変数と句を導入して加算器を明白な方法で実装することにより、上記の制約を処理していたということでした。ただし、その変換を自分で (MiniSat+ を使用して) 実行し、結果を SAT ソルバーに渡すには、Z3 よりも桁違いに時間がかかります。したがって、上記のタイプのシステムを解決するために Z3 がどのような戦略を使用するのか疑問に思っています - それは加算器を使用した変換以外のものですか?

4

1 に答える 1

0

Z3 は、この種の問題を解決するために SAT への還元を使用します。シェルを使用している場合は、オプション-v:10(詳細メッセージ) を指定できます。Z3 は、何をしているかを説明するいくつかのメッセージを表示します。あなたが説明した種類の問題について、Z3 はおそらく次の形式の詳細なメッセージを表示します。

(lia2pb :num-exprs 9 :num-asts 185 ...)
(pb2bv :num-exprs 9 :num-asts 185 ...)

lia2pbZ3 は、線形整数算術問題を疑似ブール制約問題に変換していることを意味します。そしてpb2bv、問題をビットベクトル演算に減らしていることを意味します。

lia2pb変換はファイルに実装されています : http://z3.codeplex.com/SourceControl/latest#src/tactic/arith/lia2pb_tactic.cpp

pb2bv変換はファイルに実装されています : http://z3.codeplex.com/SourceControl/latest#src/tactic/arith/pb2bv_tactic.cpp

于 2013-09-09T19:15:30.993 に答える