为什么当断言有权力时，Z3 总是返回未知

Question

这是输入

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

它几乎立即返回未知。

Answer 1

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

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

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

(check-sat-using qfnra-nlsat)

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

有关非线性整数算术和 Z3

的详细信息，请参阅此处：Z3 如何处理非线性整数算术？