哪个非线性断言在 smt/z3 优化中是完整的?

Question

我列出了一些关于二次函数的断言：

(declare-fun H () Int)
(assert (>= H 8000))
(assert (<= H 12000))
(minimize (- (^ H 2) H))
(check-sat)

但答案是"未知"，未知的原因是(不完整(理论算术((;我不明白哪个是丢失的

Answer 1

一般来说，z3 不能处理非线性项。(如果将两个变量相乘，则项是非线性的。在您的情况下，那将(^ H 2).

对于优化引擎尤其如此：整数上的非线性约束很可能是遥不可及的。但你很幸运：你的公式相当简单，所以它可以很好地处理它。使用乘法重写它：

(declare-fun H () Int)
(assert (>= H 8000))
(assert (<= H 12000))
(minimize (- (* H H) H))
(check-sat)
(get-model)

这将打印：

sat
(model
(define-fun H () Int
8000)
)