爲什麼當斷言有權力時Z3總是返回未知數？

實施例1對

(declare-var a Int) 
(declare-var b Int) 
(declare-var n Int) 
(assert (= b (* a a))) 
(assert (not (= b (^ a 2)))) 
(check-sat)

實施例2

(declare-var a Int) 
(declare-var b Int) 
(declare-var n Int) 
(assert (= b (* (^ a n) a))) 
(assert (not (= b (^ a (+ n 1))))) 
(check-sat)

它返回未知幾乎瞬間。

2016-04-23 Tom

你的問題屬於被稱爲非線性整數算術的片段，這是不可判定的。也就是說，沒有決定程序來確定查詢的可滿足性。（非線性手段，基本上沒有涉及至少兩個變量乘積項）。

話雖如此，大多數解算器確實有啓發式回答涉及非線性算術查詢，Z3也不例外。當然，作爲啓發式的，它可能會或可能不會產生答案。這就是你正在觀察的，唉，看來Z3使用的默認策略只是不足以解決你的問題。

作爲一種常見技巧，您可以嘗試Z3的非線性實數算法求解器來解決這類問題。代替check-sat，使用：

(check-sat-using qfnra-nlsat)

在這種情況下，Z3試圖解決基準假定輸入是實數，並認爲如果溶液實際上是整數。這個技巧可以成功解決一些整數非線性算術查詢，當然並不總是如此。例如，如果您在第一個示例上嘗試qfnra-nlsat，則會看到它成功地解決了這個問題，但第二個示例仍然回答unknown。

有關非線性整數運算和Z3的詳細信息，請參見：How does Z3 handle non-linear integer arithmetic?

2016-04-24 01:54:26

回答