5

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

(declare-fun p (Int) Bool)
(assert (p 0))

(assert (forall ((x Int)) 
    (=> 
    (and (> x 0) (<= x 20))
    (= (p (- x 1)) (p x) ))))
(assert (not (p 20)))

(check-sat)

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

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

(declare-fun p (Int) Bool)
(assert (p 0))

(assert (forall ((x Int)) 
    (! (=> 
    (and (> x 0) (<= x 40))
    (= (p (- x 1)) (p x) )) :pattern ((<= x 40)))))
(assert (not (p 40)))

(check-sat)

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

4

1 に答える 1

6

Z3は、多くのヒューリスティックを使用して、数量詞のインスタンス化を制御します。1つは、「インスタンス化の深さ」に基づいています。Z3は、すべての式に「depth」属性のタグを付けます。ユーザーが指定したすべてのアサーションは、深さ0でタグ付けされます。数量詞がインスタンス化されると、新しい式の深さがバンプされます。Z3は、事前定義されたしきい値よりも大きい深さでタグ付けされた式を使用して数量詞をインスタンス化しません。あなたの問題では、しきい値に達しています：(p 40)は深さ0、(p 39)は深さ1、(p 38)は深さ2などです。

しきい値を上げるには、次のオプションを使用する必要があります。

(set-option :qi-eager-threshold 100)

このオプションの例を次に示します：http：//rise4fun.com/Z3/ZdxO。

もちろん、この設定を使用すると、Z3はたとえば。のタイムアウトになり(p 110)ます。

将来的には、Z3は「有界量化」をより適切にサポートする予定です。ほとんどの場合、この種の数量詞を処理するための最良のアプローチは、それを拡張することです。プログラムAPIを使用すると、式をZ3に送信する前に簡単に「インスタンス化」できます。Pythonの例を次に示します（http://rise4fun.com/Z3Py/44lE）：

p = Function('p', IntSort(), BoolSort())

s = Solver()

s.add(p(0))
s.add([ p(x+1) == p(x) for x in range(40)])
s.add(Not(p(40)))

print s.check()

最後に、Z3では、算術記号を含むパターンはあまり効果的ではありません。問題は、Z3が解く前に数式を前処理することです。そうすると、算術記号を含むほとんどのパターンが一致することはありません。パターン/トリガーを効果的に使用する方法の詳細については、この記事を参照してください。著者はスライドデッキも提供しています。

于 2012-11-02T16:06:28.120 に答える