z3 - エンコーディングは「不明」を返します

Question

この例: http://pastebin.com/QyebfD1p z3 と cvc4 は、check-sat の結果として「unknown」を返します。どちらも原因についてあまり詳細ではありません.z3の実行についてより詳細にする方法はありますか?

Answer 1

あなたのスクリプトは戦術を使用しています

s = Then('simplify','smt').solver()

この戦術は、Z3 簡素化を適用してから、Z3 で利用可能な「汎用」SMT ソルバーを実行します。このソルバーは、非線形演算に対して完全ではありません。これは、シンプレックス、区間演算、およびグロブナー基底の組み合わせに基づいています。このモジュールの大きな制限の 1 つは、無理数を含むモデル/解が見つからないことです。将来的には、このモジュールを Z3 で利用可能な新しい非線形ソルバーに置き換える予定です。

非線形演算については、通常、Z3 で利用可能な nlsat ソルバーをお勧めします。これは完全な手順であり、通常、満足できないインスタンスと満足できるインスタンスに対して非常に効果的です。nlsat の詳細については、この記事を参照してください。nlsat を使用するには、使用する必要があります

s = Tactic('qfnra-nlsat').solver()

残念ながら、あなたの例では nlsat が動かなくなります。解決中に生成された非常に大きな多項式のサブ結果の計算がスタックします。

Z3 には、非線形演算を処理するためのエンジンがもう 1 つあります。このエンジンは、問題を SAT に減らします。a + b sqrt(2)これは、aとbが有理数である形式の解を持つ充足可能な問題に対してのみ有効です。このエンジンを使用すると、非常に短い時間で問題を解決できます。投稿の最後に結果を添付しました。このエンジンを使用するには、使用する必要があります

s = Then('simplify', 'nla2bv', 'smt').solver()

編集さらに、タクnla2bvティックは有理数をビットベクトルのペアとしてエンコードしaますb。デフォルトでは、サイズ 4 のビットベクトルを使用します。ただし、この値はオプションを使用して指定できますnlsat_bv_size。これはグローバル オプションではなく、タクティックに提供されるオプションnla2bvです。したがって、少数のビットを使用してエンコードできる形式のnla2bvソリューションのみを見つけることができます。充足可能な問題にこの形式の解がない場合、この戦術は失敗して を返します。 編集終了a + b sqrt(2)abunknown

あなたの例は、nlsat を改善し、モデル/ソリューション検索手順としてより効果的にする必要があることも示唆しています。問題に解決策がないことを示そうとすると、現在のバージョンが動かなくなります。私たちはこれらの制限を認識しており、それらを回避するための新しい手順に取り組んでいます。

ところで、Python フロントエンドでは、Z3 はモデル/ソリューションを 10 進表記で表示します。ただし、すべてが正確に計算されます。ソリューションの正確な表現を取得します。メソッドを使用できますsexpr()。たとえば、ループを次のように変更しました

for d in m.decls():
    print "%s = %s = %s" % (d.name(), m[d], m[d].sexpr())

新しいループでは、結果を 10 進数表記と内部の正確な表記で表示しています。の意味は(root-obj (+ (* 2 (^ x 2)) (* 12 x) (- 7)) 2)、多項式の 2 乗根です2*x^2 + 12x - 7。

EDIT Z3 は、重要なソルバーを作成するためのコンビネーターを提供します。上記の例ではThen、さまざまな戦術の順次構成を実行していました。OrElseまた、さまざまな戦術を試すために使用することもあります。数ミリ秒間TryFor(t, ms)戦術を試行し、指定された時間内に問題を解決できない場合は失敗します。これらのコンビネータを使用して、問題を解決するためにさまざまな戦略を使用する戦術を作成できます。 編集終了tms

sat
Presenting results
traversing model...
s_2_p_p = 0.5355339059? = (root-obj (+ (* 2 (^ x 2)) (* 12 x) (- 7)) 2)
s_1_p_p = 0 = 0.0
s_init_p_p = 0.2928932188? = (root-obj (+ (* 2 (^ x 2)) (* (- 4) x) 1) 1)
s_2_p = 0.7071067811? = (root-obj (+ (* 2 (^ x 2)) (- 1)) 2)
s_1_p = 0 = 0.0
s_init_p = 0.2928932188? = (root-obj (+ (* 2 (^ x 2)) (* (- 4) x) 1) 1)
epsilon = 0 = 0.0
p_b2_s2_s_sink = 0.9142135623? = (root-obj (+ (* 4 (^ x 2)) (* 4 x) (- 7)) 2)
p_b2_s2_s_target = 0.0857864376? = (root-obj (+ (* 4 (^ x 2)) (* (- 12) x) 1) 1)
p_b2_s2_s_2 = 0 = 0.0
p_b2_s2_s_1 = 0 = 0.0
p_a2_s2_s_sink = 0 = 0.0
p_a2_s2_s_target = 0.8284271247? = (root-obj (+ (^ x 2) (* 4 x) (- 4)) 2)
p_a2_s2_s_2 = 0.1715728752? = (root-obj (+ (^ x 2) (* (- 6) x) 1) 1)
p_a2_s2_s_1 = 0 = 0.0
sigma_s2_b2 = 1 = 1.0
sigma_s2_a2 = 0 = 0.0
p_b1_s1_s_sink = 1 = 1.0
p_b1_s1_s_target = 0 = 0.0
p_b1_s1_s_2 = 0 = 0.0
p_b1_s1_s_1 = 0 = 0.0
p_a1_s1_s_sink = 1 = 1.0
p_a1_s1_s_target = 0 = 0.0
p_a1_s1_s_2 = 0 = 0.0
p_a1_s1_s_1 = 0 = 0.0
sigma_s1_b1 = 0 = 0.0
sigma_s1_a1 = 1 = 1.0
p_sinit_sink = 0.7071067811? = (root-obj (+ (* 2 (^ x 2)) (- 1)) 2)
p_sinit_target = 0.2928932188? = (root-obj (+ (* 2 (^ x 2)) (* (- 4) x) 1) 1)
p_sinit_2 = 0 = 0.0
p_sinit_1 = 0 = 0.0
s_sink = 0 = 0.0
s_target = 1 = 1.0
s_2 = 0.0857864376? = (root-obj (+ (* 4 (^ x 2)) (* (- 12) x) 1) 1)
s_1 = 0 = 0.0
s_init = 0.2928932188? = (root-obj (+ (* 2 (^ x 2)) (* (- 4) x) 1) 1)

編集 戦術を使用して、コメントの問題を解決できます

s = Then('simplify', 'nlsat').solver()

この戦術は数秒で問題を解決し、投稿の最後に解決策を生成します. 上で述べたように、これnlsatで完了ですが、非常に時間がかかる場合があります。あなたの問題は、現在のバージョンの Z3 が自動的に決定/解決できる範囲の端にあります。さまざまな戦術をOrElseand と組み合わせTryForて、より安定させることができます。例：

s = OrElse(TryFor(Then('simplify', 'nla2bv', 'smt', 'fail-if-undecided'), 1000),
           TryFor(Then('simplify', 'nlsat'), 1000),
           TryFor(Then('simplify', 'nla2bv', 'smt', 'fail-if-undecided'), 10000),
           Then('simplify', 'nlsat')).solver()

上記の戦術は、nla2bvアプローチを 1 秒、次にnlsat1 秒、次にnla2bv10 秒、最後nlsatにタイムアウトなしで試行します。

これが理想的な解決策ではないことはわかっていますが、非線形演算の次のソルバーの準備が整うまで、そのようなバリエーションは有用な回避策になる可能性があります。さらに、Z3 には、呼び出す前に問題を単純化/前処理するために使用できる他の多くの戦術がありますnlsat。 編集終了

s_init = 15/32
s_1 = 7/16
s_2 = 1/2
s_target = 1
s_sink = 0
p_sinit_1 = 1/2
p_sinit_2 = 1/4
p_sinit_target = 1/8
p_sinit_sink = 1/8
sigma_s1_a1 = 1/2
sigma_s1_b1 = 1/2
p_a1_s1_s_1 = 1/2
p_a1_s1_s_2 = 1/4
p_a1_s1_s_target = 1/8
p_a1_s1_s_sink = 1/8
p_b1_s1_s_1 = 1/2
p_b1_s1_s_2 = 1/4
p_b1_s1_s_target = 1/16
p_b1_s1_s_sink = 3/16
sigma_s2_a2 = 1/2
sigma_s2_b2 = 1/2
p_a2_s2_s_1 = 1/2
p_a2_s2_s_2 = 1/4
p_a2_s2_s_target = 11/64
p_a2_s2_s_sink = 5/64
p_b2_s2_s_1 = 3/4
p_b2_s2_s_2 = 1/32
p_b2_s2_s_target = 9/64
p_b2_s2_s_sink = 5/64
epsilon = 1/4
s_init_p = 1649/3520
s_1_p = 797/1760
s_2_p = 103/220
s_init_p_p = 1809/3904
s_1_p_p = 813/1952
s_2_p_p = 127/244

EDIT 2 あなたの問題は、Z3が妥当な時間内にできることの限界にあります。非線形実数演算は決定可能ですが、非常にコストがかかります。Z3で何が起こっているかのデバッグ/トレースについて。以下にいくつかの可能性を示します。

• コマンドを使用して詳細メッセージを有効にすることができます: set_option("verbose", 10). 数値は冗長レベルです: 0 == 「メッセージなし」、数値が大きい == 「メッセージが多い」。

• トレースをサポートして Z3 をコンパイルします。詳細については、この投稿を参照してください。

• コマンドを使用して、Python プログラムによって呼び出された Z3 API のログを作成しますopen_log("z3.log")。このコマンドは、他の Z3 API 呼び出しの前に呼び出す必要があります。z3次に、内の実行可能ファイルを使用してログを実行しますgdb。そのため、実行を停止して、Z3 がスタックしている場所を見つけることができます。通常、nlsatソルバーは次の 2 つの場所でスタックします。

  1. サブ結果の計算 (手続きpsc_chainはスタックに置かれます)、および

  2. 代数係数を持つ多項式の根を分離します (手順isolate_rootsはスタック上にあります)。

問題 2 は、古い代数パッケージをはるかに効率的な新しいものに置き換えた後、すぐに修正されます。残念ながら、問題はサブ結果ステップでスタックしているようです。

別の注意:nla2bv元のベンチマークでは効果的でしたが、新しいベンチマークa + b sqrt(2)でaとbが有理数であるという形式の解が得られる可能性は低いです。したがって、使用nla2bvは単なるオーバーヘッドです。この戦術nlsatは、問題が CNF にあると想定しています。したがって、 forpastebin.com/QRCUQE10を呼び出すtseitin-cnf前に呼び出す必要がありnlsatます。別のオプションは、「大きな」戦術を使用することqfnra-nlsatです。を呼び出す前に、多くの前処理ステップを呼び出しnlsatます。ただし、これらの手順によっては、問題の解決が難しくなる場合があります。

編集終了 2