問題タブ [smt]

私は、用語の書き換えを使用して固定サイズのビットベクトル算術問題を解決/簡素化することに焦点を当てたプロジェクトに取り組んでいます。これは、ビットブラストに基づくものなどの決定手順の前のステップとして役立つものです。書き換えという用語は、問題をまったく解決するか、そうでなければ、はるかに単純な同等の問題を生成する可能性があるため、両方を組み合わせると、かなりの速度向上が得られます。

多くの SMT ソルバーがこの戦略を実装していることは承知しています (Boolector、Beaver、Alt-Ergo、Z3 など)。一般に、著者がそのような単純化の手順をいくつかの段落で説明している論文しか見つけられませんでした。用語の書き換えの使用法を詳細に説明しているドキュメントを見つけたいと思います: ルールの例を提供し、AC 書き換えおよび/または他の等式公理の利便性について議論し、書き換え戦略の使用など.

今のところ、CVC Lite によって実行される正規化/単純化の手順について説明しているテクニカル レポートA Decision Procedure for Fixed-Width Bit-Vectorsを見つけました。このようなテクニカル レポートをもっと見つけたいと思います! STP での用語の書き換えに関するポスターも見つけましたが、これは簡単な要約にすぎません。

私はすでにそれらの SMT ソルバーの Web サイトにアクセスし、それらの出版物ページを検索しました...

よく知られているSMTソルバーの現在のバージョンで用語の書き換えがどのように使用されているかについての参照または説明をいただければ幸いです。Z3 は最もスマートな単純化フェーズの 1 つを備えているように見えるので、特に Z3 に興味があります。たとえば、Z3 3.* では新しいビット ベクトル決定手順が導入されましたが、残念ながら、それについて説明している論文を見つけることができませんでした。

smt-lib2 を使用して数式の最大値を取得するにはどうすればよいですか?

私はこのようなものが欲しい：

もちろん、'max' は smtlibv2 にはわかりません。では、どうすればこれを行うことができますか？

Z3の列挙型間のサブタイプ関係を表現するための最良の方法は何ですか？

具体的には、次のようなことをしたいと思います。

次に、新しいサブタイプを作成します。

そのため、動物タイプの4つの異なる定数があるという主張はSATですが、哺乳類タイプの4つの異なる定数があるという主張はUNSATです。

属性値を計算するにはどうすればよいですか? 次に例を示します。

これで私は2つのモデルを取得します:

今、私が欲しいのは次のようなものです：

したがって、属性の合計が 6 より大きいモデルを取得したいと思います。

たぶん、配列を操作することがこれを達成する方法です...

これは主に論理的な問題だと思います...

私はこの smtlib 式を使用します:

この構造の用語はどれですか（少なくとも私の意見では）：

私の推測: resultSet は次のようになります。

しかし、これはscala^z3 ctx.checkAndGetAllModels()を使用しています:

ad と abcd が入っているのはなぜですか? 期待した結果だけを得ることができますか?

編集の理由により、解決する大きなブール式があります。ここに画像を貼り付ける必要があります。

areaまた、 4 つの整数の次元を測定する関数が既にあります。area(c,d,e,f)=|c−d|×|e−f|

数式が満足できるかどうかを判断するだけ(a,b,c,d,e,f)ではなく、大きな数式を作成し、数式を満たす他の 6 タプルの次元以上の最適な 6 タプルをTRUE探しarea(c,d,e,f)ています。

言い換えれMax(area(c,d,e,f))ば、大きな公式の対象を見つけてください。

SMT ソルバーがこの問題に役立つかどうか疑問に思っています。Z3が をサポートしていることを学びquantifiers、ブール式が満足できるかどうかを判断できるようになりました。しかし問題はZ3、関数の最適解を見つけるのに役立つかどうかareaです。

誰にもアイデアはありますか？SMT ソルバー、Z3、またはその他のアルゴリズムについてのコメントをお待ちしております...

ブール式の最適化問題z3を解決することを目的としたコードがあります

量指定子と含意のためだと思いますが、このコードには多くのコストがかかります。オンラインでテストしたところ、2 つの警告が表示され、最終結果はunknown次のようになりました。

良い結果が得られないのがこれらの2つの警告であるかどうか、誰か教えてもらえますか? このコードを最適化して実行する方法はありますか?

私はこの次のコードを持っています

コードは最初にunsat（check-sat）を返し、2番目にsat（check-sat）を返すはずですが、不明になります。

誰かが何が問題なのか教えてもらえますか？私はWindows7を使用していますが、cygwinを使用してjSMTLIBを使用しています

ありがとうサイフ

SMTLIB配列を使用しているときに、Z3の理論の理解と私の理解の違いに気づきました。私は公式ウェブサイト[1]にあるSMTLIB配列理論[0]を使用しています。

私の問題は簡単な例で最もよく説明されていると思います。

最初の配列はインデックス1で2を返し、他のすべてのインデックスでは0を返し、2番目の配列はインデックス0で1を返し、インデックス1で2を返し、他のすべてのインデックスで0を返す必要があります。selectインデックス0で呼び出すと、これを確認できるようです。

Z3はsat両方に戻ります。

予想通り、この場合、Z3（重要な場合はlinux-amd64でバージョン3.2を使用しています）が応答unsatします。次に、これら2つのアレイを比較してみましょう。

Z3はsat、「これら2つの配列は同等に比較される」と解釈します。ただし、これらの配列は同等に比較されないと思います。私はこれをSMTLIB配列理論に基づいています。

したがって、平易な英語では、これは「2つの配列は、すべてのインデックスで等しい場合にのみ、等しいと比較される」という意味になります。誰かが私にこれを説明できますか？私は何かを見逃しているのですか、それとも理論を誤解していますか？この問題についてのご意見をお待ちしております。

よろしく、レオン

[0] http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2 [1] http://smtlib.org

最小の 4 つの整数値を返す関数を SMT 2.0 で定義したいと考えています。