3

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

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

(assert (! (disjoint_1 B A) :named a2 ))
(assert (! ; axiom for "disjoint_1"
    (forall ((A Rel1)(B Rel1)) (= 
        (disjoint_1 A B) 
        (forall ((a0 Atom)) (not (and (in_1 a0 A) (in_1 a0 B)))))) 
:named ax8))

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

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

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

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

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

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

4

1 に答える 1

4

Z3 4.x は、量指定子を処理するために、EMatching と MBQI (Model Based Quantifier Instantiation) の 2 つのメイン エンジンを使用します。EMatching エンジンは、満足できないインスタンスに対してのみ有効です。つまり、数式 (量指定子を含む) が充足可能であることを示すことはできません。一方、MBQI ではそれが可能です。実際には、多くの有用なフラグメントを決定できます。Z3 ガイド(量指定子のセクション) では、これらのフラグメントの一部について説明しています。そうは言っても、Z3には一次論理用の有限モデルファインダーがありません（Paradoxなど）。これは便利な機能であり、今後追加される可能性があります。メッセージの例は、Z3 を使用して解決できます。ここで試すことができます。

パターンに関しては、EMatching エンジンの「ヒント」です。EMatching エンジンは問題が充足可能であることを示すことができないため、実際には役に立ちません。満足できるインスタンスの場合、パターンを追加できます。これは、EMatching エンジンがインスタンスを生成しすぎて MBQI エンジンの邪魔にならないようにするためです。または、量指定子の単純なインスタンスをアサートすることにより、探索空間を熱心に刈り込みたいと考えています。オプションを使用して EMatching エンジンを無効にすることもできます(set-option :ematching false)。

(declare-sort Rel1)
(declare-sort Atom)
(declare-fun disjoint_1 (Rel1 Rel1) Bool)
(declare-fun in_1 (Atom Rel1) Bool)
(declare-const A Rel1)
(declare-const B Rel1)

(assert (! (disjoint_1 B A) :named a2 ))
(assert (! ; axiom for "disjoint_1"
    (forall ((A Rel1)(B Rel1)) (= 
        (disjoint_1 A B) 
        (forall ((a0 Atom)) (not (and (in_1 a0 A) (in_1 a0 B)))))) 
:named ax8)) 

(check-sat)
(get-model)
于 2012-10-23T14:31:47.667 に答える