問題タブ [smt]

このチュートリアルに続いて、チュートリアルのこの最初の例を試しました。

このコマンドを実行しました

チュートリアルのように取得しunknownないため。unsat

これの何が問題になっているのでしょうか？

私はsatソルバーのコンテキストでこの質問をしています。x1, x2, x3 ... x100の間にランダムに値が割り当てられた100個の整数変数があるとします1 to N。x1 to x100の少なくとも1つの変数がからの値のそれぞれを持っていることを確認したいと思います1 to N。

ここで、この問題をsatソルバー制約でエンコードしたいと思います。制約を書いている間、私は値を知らないので、N以下のようにコーディングするのは難しいです-

最後に、Nの値を2と主張すると、上記の制約は機能しなくなります。さらに、パフォーマンス上の理由から、配列や解釈されていない関数は使用したくありません。

アップデート ：

要するに、制約は次のとおりです-

1. N <100
2. （N = 20としましょう）、20個の変数があり、それらはx_1からx_100までのいずれかである可能性があります。したがって、この制約により、1からNまでの値ごとに少なくとも1つの変数が割り当てられるようになります。
3. 残りの変数（100-N）の値は互いに重複する可能性があります。

誰かが私にいくつかの提案をすることができますか？

Z3定理証明者を使用して、満足のいく割り当てのセットから均一にサンプリングする方法はありますか? そうでない場合、この機能を備えた Z3 に最も近いシステムはどれですか?

Microsoft の Z3 SMT ソルバーを使用しており、カスタム ソートの定数を定義しようとしています。そのような定数はデフォルトでは等しくないようです。次のプログラムがあるとします。

もちろん、同じ種類の 2 つの定数が等しいことは完全に可能であるため、これは "sat" を返します。定数が互いに異なる必要があるモデルを作成しているので、これは、フォームの公理を追加する必要があることを意味します

同じ種類の定数のすべてのペアに対して。ソートの各定数がデフォルトで一意になるように、このジェネリックを行う方法があるかどうか疑問に思っていました。

パラメータ化された並べ替えの値にアクセスするにはどうすればよいですか?

たとえば、次の宣言があるとします。

xを表すペアの最初の要素にアクセスするにはどうすればよいですか?

テンプレートから問題を生成しますが、問題の性質上、量指定子に頼らざるを得ません。これで、ソルバーは本当に単純な (満足できる) 問題のインスタンスのみを見つけることができます。多くの場合、「unsat」の検索は機能します。「sat」を見つけることはめったに機能しません。

問題は、互いに素な 2 つのセットの定義のような単純なものでさえ、いくつかの非常にやっかいな式で表現しなければならないことです。

(ここで完全な問題を見つけてください)

インスタンスを見つけるために、Z3 は関数の解釈を見つけなければなりませんin_1。他のすべての機能はすべてそれに依存しています。

これまでのところ、私の問題に関連して次のような発言を聞いています。

1. すべての量指定子にはパターンが必要です
2. 無限モデルがある場合、インスタンス検索は機能しません

これを達成または回避する方法について、ウェブや文献で役立つ情報を見つけることができませんでした。だから私の質問は残ります：

(Z3 を使用して) 充足可能な数式のインスタンスを効率的に見つけるにはどうすればよいですか? パターンを使用してこれを達成するにはどうすればよいですか (ある場合)。

.NETAPIで作成された既存のZ34.1コンテキストがあり、多くの関数宣言、ソート宣言、仮定がアサートされています。

このコンテキストで既存のすべての宣言を使用してSMT-LIB2文字列を解析する最もクリーンな方法は何ですか？具体的には、コンテキスト内のすべての宣言を繰り返す方法はありますか？宣言にアクセスできるようにするメソッドがContextに表示されませんでした。

現在、私は次のことを行っています。

これらすべての宣言とシンボル名をz3コンテキスト自体から取得する方法はありますか？それらはすべて、z3オブジェクトですでに宣言されています。内部データ構造を反復処理するよりも、この方法で実行したいと思います。

私はそれを見逃したかもしれませんが、APIでこれを行うことができるものは何も見つかりませんでした。Solver.Assertionsを介して利用できるアサートされた数式の配列に似たものをイメージしています。

定理証明ツールz3は、数式を解くのにかなりの時間がかかります。これは、簡単に処理できるはずです。これをよりよく理解し、おそらくz3への入力を最適化するために、z3が解決プロセスの一部として生成する内部制約を確認したいと思いました。コマンドラインからz3を使用する場合、バックエンドソルバー用にz3が生成する数式を出力するにはどうすればよいですか？

Microsoft が開発した SMT ソルバーである Z3 に 1 次理論を入れたいと考えています。この理論には、オブジェクトobj1とobj2の 2 つのオブジェクトがあり、オブジェクトを受け取りアクションを返す関数moveと、アクションを引数として取る1 位の述語が発生します。理論には数式occurs(move(obj1)) が含まれており、これが発生述語が真になる唯一の方法であることを確認したいと思います。私は発生の定義を与えることによってこれを行います:

これは、ocens(move(obj1))は理論から推論できますが、ocens(move(obj2))は推論できないことを意味します。これを証明するために、私はこれを次のように Z3 に翻訳しました。

問題は、これにより次の出力が得られることです。

私には理解できません。発生の定義は、述語が真になるための必要かつ十分な条件をすべて提供するため、どのモデルでも発生(move(obj2))が真になることはできないと思います。私は何を間違っていますか？

更新 de Moura のおかげで、問題の解決策を見つけることができました。私がする必要があるのは、アクション (私の場合は関数) に固有の名前の公理を提供することです。2 つの異なる引数がある場合、 sort の同じ要素を決して返さないことmoveを述べる必要があります。これはいくつかの方法で実行できますが、これが最も簡潔なバージョンであることがわかりました。moveAction

私は、マイクロソフトのSMTソルバーであるZ3で帰納的事実を証明しようとしています。Z3ガイド（セクション8：データ型）で説明されているように、Z3は一般にこの機能を提供しないことを知っていますが、事実を証明したいドメインを制約すると、これが可能になるようです。次の例を考えてみましょう。

ソルバーは、で正しく応答します。unsatこれは、それが有効であることを意味し(p 20)ます。問題は、この制約をさらに緩和すると（20前の例では、20より大きい整数に置き換えます）、ソルバーが。で応答することunknownです。

元の問題を解決するのにZ3に時間がかからないので、これは奇妙だと思いますが、上限を1つ上げると、突然不可能になります。次のように、数量詞にパターンを追加しようとしました。

どちらがうまくいくように見えますが、現在の上限は40です。これは、Z3を使用してそのような事実を証明できない方がよいということですか、それとも問題を誤って定式化したのでしょうか。