为什么 Z3 在断言有效时总是返回未知？答案

【问题标题】：Why Z3 always return unknown when assertions have power?为什么 Z3 在断言有效时总是返回未知？
【发布时间】：2016-04-23 15:40:00
【问题描述】：

这是输入

示例 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)

它几乎立即返回未知。

【问题讨论】：

标签： z3 smt

【解决方案1】：

您的问题属于称为非线性整数算术的片段，这是不可判定的。也就是说，没有决策过程来确定查询的可满足性。（非线性基本上意味着有一个乘法项涉及至少两个变量。）

话虽如此，大多数求解器确实有启发式来回答涉及非线性算术的查询，Z3 也不例外。当然，作为一种启发式方法，它可能会也可能不会产生答案。这就是您所观察到的，可惜 Z3 使用的默认策略似乎不足以解决您的问题。

作为一个常见技巧，您可以尝试使用 Z3 的非线性实数求解器来解决这类问题。代替check-sat，使用：

(check-sat-using qfnra-nlsat)

在这种情况下，Z3 尝试在假设输入为实数的情况下求解基准，并查看解是否实际上是整数。这个技巧可以成功地解决一些整数非线性算术查询，但当然并非总是如此。例如，如果您在第一个示例中尝试 qfnra-nlsat，您会看到它成功解决了它，但它仍然会在第二个示例中回答 unknown。

关于非线性整数运算和Z3的详细信息，请看这里：How does Z3 handle non-linear integer arithmetic?

【讨论】：