1

次の SMTLIB プログラムを検討してください (rise4fun here で):

(set-option :auto_config false)
(set-option :smt.mbqi false)
(set-option :smt.arith.nl.gb false)

(declare-const n Int)
(declare-const i Int)
(declare-const r Int)

(assert (= i n))
(assert (= r (* i n)))

(push)
(assert (not (= r (* n n))))
(check-sat) ; unknown
(pop)

Z3 (4.3.2 公式リリース、および 4.4.0 b6c40c6c0eaf) は、構文上の同等性に関する推論のみを必要とするように見えますが、最終的なアサーションが であることを示していませんunsat。

予想外に（少なくとも私にとっては）、に設定smt.arith.nl.gbするtrueと、例が検証されます（つまり、check-satyields unsat）。

それだけの価値があるため、さらにいくつかの観察結果を次に示します。

  • 乗算がまたはにそれぞれ変更された場合、最終的なアサーションを示すことができます。unsat(* i n)(* n i)

  • 乗算を次のように変更すると表示できません。unsat(* i i)

  • (push)例に(pop)影響を与えるようには見えません。つまり、記述された観察に影響を与えずに削除できます。

smt.arith.nl.gbこれはバグですか、それともこの例を表示する必要がある理由はありunsatますか?

4

1 に答える 1

2

これは必ずしもバグではありません。Groebner 基底計算は問題を解決するので、unsat の結果はすぐに見つかります (これは良いことなので、デフォルトで有効になっています)。さらに、auto_config を無効にすることは、問題に応じて他のオプションのホストが設定されないことも意味します (ただし、この特定のケースでは違いはありません)。

一部のタクティック、ソルバー、または単純化者は、問題がたまたま人間や他のソルバーにとって解決しやすいかどうかに関係なく、乗算式を見ると単純に諦めてしまうことに注意してください。この特定のケースでは、smt.arith.nl.rounds が使い果たされた後 (デフォルトでは 1024)、非線形ソルバーは諦め、unknown を返します。

この問題をすばやく解決するタクティックの 1 つは solve-eqs ですが、これはデフォルトのタクティックの一部ではありません (この場合は qfnia タクティックを実行します)。問題が解決する場合は、check-sat コマンドを次のように置き換えることで簡単に追加できます。

(check-sat-using (then solve-eqs qfnia))

これがデフォルトであるべきかどうかは議論の余地があり、ベンチマークまでですが、実際にはバグではありません。

この問題をすばやく解決する別の戦術は、NLSAT ソルバーです。

(check-sat-using nlsat)
于 2015-01-29T18:01:09.353 に答える