2

2つのSMT問題インスタンスがあります。最初はここにあります：

http://gist.github.com/1232766

Z3は、私のそれほど優れていないマシンで約2分でこの問題のモデルを返します。これは素晴らしいです。私もこれを持っています：

http://gist.github.com/1232769

Z3を完了せずに、この問題でz3を一晩実行しました。これらのファイルの内容を確認すると、最初のインスタンスによって返されたモデルを「拒否」する追加のアサーションがあることを除いて、2番目のファイルが最初のファイルと同じであることがわかります。（私が何を意味するかを確認するために、それらの間で「差分」を行うことができます。）この問題には複数の満足のいくモデルがあることを偶然知っており、z3を使用してすべての満足のいくモデルを見つけようとしています。

これは完全に予想されることかもしれませんが、2番目の問題が最初の問題と比較してZ3にとってはるかに難しい問題である理由を知りたいと思いました。Z3がより簡単な時間を持てるように、2番目の問題を定式化するためのより良い方法はありますか？

ありがとう..

4

1 に答える 1

2

あなたのアプリケーションについてもっと知らずにあなたに正確な答えを与えるのは難しいです。ご提案のとおり、モデリングは、使用しているロジックで大きな役割を果たしますAUFBV。Z3で使用される戦略も、全体的なパフォーマンスに大きな影響を与えます。Z3には、いくつかの組み込み戦略が備わっています。検索に影響を与えるために使用できる多くのパラメーターがあります。Z3には戦略仕様言語もあります。これは新機能です。進行中のため、宣伝はしていません。言語は次のバージョンで変更される可能性があります。次のコマンドを実行すると、戦略言語に関する詳細情報にアクセスできます。

(help check-sat-using)
(help-strategy)

そうは言っても、Z3には、問題に効果的であると思われる組み込みの戦略があります。これは、ロジックに使用される戦略UFBVです。問題は配列を使用していますが、table0を2つの引数を持つ関数に変換することで回避できます。

(declare-fun table0 ((_ BitVec 64) (_ BitVec 64)) (_ BitVec 8))

そして、フォームのすべての用語を、任意の用語(select (table0 s65) t)で(table0 s65 t)あるwhereに置き換えます。最後に、ファイルの先頭にtもコマンドを追加する必要があります。(set-logic UFBV)この設定で、クエリ用に4つの異なるモデルを生成することができました。それ以上生成しようとはしませんでした。各呼び出しは約75秒を消費しました。

于 2011-09-21T20:26:16.403 に答える