在 Z3 中无法解决。为什么？答案

【问题标题】：Not Solvable in Z3. Why?在 Z3 中无法解决。为什么？
【发布时间】：2017-07-20 17:00:55
【问题描述】：

在 Z3 中无法解决。为什么？

我的程序：

;x = 2x + 2 (This on Underlaying DB is always increasing as X > Y in DB)
(declare-const x0 Real)
(declare-const xn Real)
(declare-const n Real)
(push)
(assert (= x0 42))
(assert (= xn (+ (* x0 (^ 2 n)) (* 2 (- (^ 2 n) 1)) ) )) ; recurrence relation
(assert (> xn 700))
(check-sat-using qfnra-nlsat)
(get-model); to find a satisfiable valuation
(pop); removes any assertion


-----------------------------
Z3 Answer:
-----------------------------


 unknown 
    (model 
    (define-fun n () Real 0.0) 
    (define-fun xn () Real 42.0) 
    (define-fun x0 () Real 42.0) 
    )

我也尝试过使用整数：根据数据库中的值'n'应该是4，但它是0。

请查看它，请任何人帮助我。

【问题讨论】：

unknown 可能是由于使用了非线性算术（无法确定）。此外，如果一个问题有多种解决方案，您只会得到其中一个。您的“数据库解决方案”是唯一可能的解决方案吗？
是的，数据库解决方案是唯一的解决方案！

标签： z3

【解决方案1】：

unknown 表示该模型是“被指控的”，即可能正确也可能不正确。由于您的问题包含非线性项（求幂），因此这是意料之中的。

确实，模型建议 xn = 42，这与您程序中的假设 xn > 700 相矛盾。给出的模型是假的。但是你不能为此责怪 z3，因为它已经告诉你 unknown。解决您的查询超出了 Z3 的能力。

【讨论】：

谢谢@levent