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

Question

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

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

但答案是“未知”，而未知的原因是（不完整（理论算术））；我不知道哪一个是丢失的]

Answer 1

通常，z3无法处理非线性项，尤其是在存在整数非线性约束的情况下，优化将是遥不可及的。 （如果将两个变量相乘，则该项是非线性的。）

但是您很幸运，因为您的公式很简单。使用乘法重写它：

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