数量子とパターン（QBF式）

Question

私はz3のsmt-lib 2構文でQBFをエンコードしようとしています。警告

WARNINGでZ3結果を実行：

：（！14 k個の数量詞のID）と充足結果が "不明" である数量詞のためのパターンを見つけることができませんでした。私は座って、クエリの

(set-option :auto-config false) 
(set-option :mbqi false) 
(declare-fun R (Bool Bool Bool Bool) Bool) 
(declare-fun x1() Bool) 
(declare-fun x2() Bool) 
(declare-fun x3() Bool) 
(declare-fun y() Bool) 
(assert 
    (forall ((x2 Bool) (x3 Bool)) 
    (! 
    (exists ((y Bool)) 
    (! 
     (forall ((x1 Bool)) 
     (! 
     (R x1 x2 x3 y) 
     :pattern((R x1 x2 x3 y))) 
    ) 
    :pattern((R x1 x2 x3 y))) 
    ) 
    :pattern((R x1 x2 x3 y))) 
) 
) 
(check-sat) 

結果にコードを書き換えることで警告を処分した

(declare-fun R (Bool Bool Bool Bool) Bool) 
(assert 
    (forall ((x2 Bool) (x3 Bool)) 
    (exists ((y Bool)) 
     (forall ((x1 Bool)) 
     (R x1 x2 x3 y) 
    ) 
    ) 
) 
) 
(check-sat) 

、しかし、「未知」のままで次のように

コードがあります。

パターンを正しく取得する必要があると思いますか？どのようにネストされた量指定子に指定するのですか？ただし、パターンの注釈を付けなくても、量子を使った簡単な例が動作するようです。

What is the reason behind the warning message in Z3: "failed to find a pattern for quantifier (quantifier id: k!18) "とz3ガイドへの回答があまりにも助かりませんでしたが、残念です。

Answer 1

この警告メッセージは無視できます。 E-matchingエンジンがこの定量化された式を処理できないことを通知するだけです。

電子一致は、問題が満足できないことを示すためにのみ有効です。あなたの例は充足しているので、Eマッチングはあまり役に立ちません。つまり、Z3はEマッチングエンジンを使用してsatを返すことができません。モデルベースの定量化器インスタンス化（MBQI）は、定量化器を含む問題が充足可能であることを示すことができるZ3の唯一のエンジンです。

デフォルト設定を使用すると、Z3はあなたの例としてsatを返します。 MBQIモジュールを無効にしたため、unknownが返されます。

MBQIエンジンは、Z3が多くのフラグメントの決定プロシージャであることを保証します（http://rise4fun.com/Z3/tutorial/guide参照）。しかし、一般的には非常に高価であり、迅速かつ近似的な回答で十分でない場合は無効にする必要があります。この場合、unknownはprobably satと読み取ることができます。 VCCなどの検証ツールでは、MBQIモジュールが生成する式を決定できないため、MBQIモジュールを無効にします。つまり、VCCによって生成された式は、MBQIエンジンによって決定できるフラグメントのいずれにもありません。 断片Z3の任意の数式がsatまたはunsatを返す（つまり、unknownを返さない）とき、Z3によって断片を決定することができます。もちろん、この主張は無制限の量のリソースがあることを前提としています。すなわち、Z3は、メモリが不足しているか、またはユーザによってタイムアウトが指定されたときに、決定可能なフラグメントに対して失敗（すなわち、unknownを返す）することもできる。

最後に、Z3 3.2は、MBQIエンジンにbugを持ちます。バグは修正されており、問題には影響しません。必要があれば、バグ修正が含まれたZ3 4.0のプレリリース版を提供することができます。