z3 smt証明書がこのような簡単な式で失敗するのはなぜですか？

Question

私は、私の卒業論文に取り組んでいる間、Microsoftのz3 smtプロバ私の使用例では、量子を含む簡単な式（等価を持つ一次論理）の充足可能性（モデルなし）をチェックする必要があります。 Z3は、このいずれかを除いて、ミリ秒単位のカップルで、私の例のすべてを解決する良い仕事を行います

forall x P(f(g(f(x)))) and not P(f(g(h(c)))) 

私はrise4fun.comにし、自分のコンピュータ上で式をテストした（16.04 Ubuntuの、4倍の3.4GHz以上） z3 java-bindingを使用します。私は結果を出さずに1時間後にプロセスを終了した。 私は、このような問題は半分しかないことを認識しています。 しかし、この特定の数式ではなぜz3が失敗するのですか？私は多くの他の数式（小さなものとそれ以上のもの）をテストし、z3はそれらのすべてに成功しました。 z3ではこの式を難しいものにしてくれるかもしれないと私は説明できますか？ z3の内部ではどうなりますか？

例えば：1つの関数シンボルを変更すると、（UNSAT /土）Z3は結果で終了させるのに十分である：

forall x P(f(g(f(x)))) and not P(f(g(f(c)))) 
forall x P(f(g(f(x)))) and not P(f(g(g(c)))) 
forall x P(f(g(f(x)))) and not P(f(f(g(c)))) 
forall x P(f(g(f(x)))) and not P(f(g(i(c)))) 
// and even 
forall x P(f(g(h(x)))) and not P(f(g(f(c)))) 

あなたは、次のスニペットを使用してhttp://rise4fun.com/Z3上で、これらの例を試すことができます。

(declare-fun c() Int) 
(declare-fun d() Int) 
(declare-fun f (Int) Int) 
(declare-fun g (Int) Int) 
(declare-fun h (Int) Int) 
(declare-fun i (Int) Int) 
(declare-fun P (Int) Bool) 

(assert (forall ((x Int)) 
    (P (f (g (f x))) ) 
)) 

(assert (not 
    (P (f (g (h c))) ) 
)) 

(check-sat) 

Answer 1

Z3は、あなたの定量化された式のための有限表現の解釈を見つけようとしますが、1を構築したり、式が充足不能であることを立証するために失敗しました。 公理プロファイラ：http://vcc.codeplex.com/を使用して、インスタンス化をZ3でプロファイルできます。