爲什麼z3 smt證明者失敗了這樣一個簡單的公式？

我在使用我的碩士論文的同時，用微軟的z3 smt證明器做了一些實驗。在我的用例中，我需要檢查包含量詞的簡單公式（不等式的一階邏輯）的可滿足性（無模型）。 Z3的也是一個不錯的工作解決了我所有的例子在幾毫秒，除了這一個：爲什麼z3 smt證明者失敗了這樣一個簡單的公式？

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

我所測試的配方上rise4fun.com和我的電腦上（Ubuntu的16.04，3.4GHz的4倍）使用z3的java綁定。我在1小時後殺死了這個過程，沒有任何結果。我意識到這樣的事實，這種問題只有半可判定性。但是爲什麼z3對這個特定的公式失敗。我測試了很多其他公式（小一些甚至更大的公式），並且z3在所有公式中都成功。也許人們可以向我解釋是什麼讓這個公式對z3很難？ z3內部會發生什麼？

例如： - 改變一個函數符號是足以讓Z3與結果終止（SAT /不飽和度）：

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)

來源

2016-09-27 Zerlono

Z3試圖爲您的量化公式找到有限可解釋的解釋，但未能建立或解釋公式不可滿足。您可以使用公理分析器對Z3的實例進行剖析：http://vcc.codeplex.com/。

來源

2016-09-27 15:21:56

但是在這種情況下，z3在相似的公式上也會失敗。但事實並非如此。此外，這個公式沒有嵌套的量詞（在一個謂詞上只有一個量詞）。所以我想這對於Z3來說應該是一個簡單的運行，至少通過嘗試所有可能的組合來解決它至少需要幾毫秒 – Zerlono

爲什麼z3 smt證明者失敗了這樣一個簡單的公式？

回答

相關問題