7

z3のsmt-lib2構文でQBFをエンコードしようとしています。z3を実行すると、警告が表示されます

警告：数量詞のパターンが見つかりませんでした（数量詞ID：k！14）

充足可能性の結果は「不明」です。

コードは次のとおりです。

(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)

コードを次のように書き直すことで警告を取り除きました

(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)

ただし、sat-queryの結果は「不明」のままです。

パターンを正しくする必要があると思いますか？ネストされた数量詞にそれらを指定するにはどうすればよいですか？ただし、数量詞を使用した単純な例は、パターン注釈がなくても機能するようです。

Z3の警告メッセージの背後にある理由は何ですか：「数量詞（数量詞id：k！18）のパターンを見つけることができませんでした」とz3ガイドは残念ながらあまり役に立ちませんでした。

4

1 に答える 1

8

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

E マッチングは、問題が満たされないことを示す場合にのみ有効です。あなたの例は満足できるので、Eマッチングはあまり役に立ちません。つまり、Z3 はsatE マッチング エンジンを使用して戻ることができなくなります。モデルベースの量指定子のインスタンス化 (MBQI) は、量指定子を含む問題が充足可能であることを示すことができる Z3 の唯一のエンジンです。

デフォルトの構成を使用すると、Z3 がsat例に戻ります。unknownMBQIモジュールを無効にしたため、返されます。

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

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

于 2012-04-05T18:15:00.750 に答える