SMT/Z3 Optimizer完备非线性断言咨询及二次函数优化问题求助

1. SMT/Z3 Optimizer中哪种非线性断言是完备的？ #

得先明确：Z3对非线性算术的支持分实数域和整数域两种情况，差异非常大：

• 非线性实数算术：对于仅包含实数变量、多项式等式/不等式的约束（比如二次、高次多项式约束），Z3的非线性实数求解器在绝大多数实际场景下是完备的。这是因为实数上的多项式约束可以通过圆柱代数分解（CAD）等成熟算法处理，虽然理论上非线性实数算术属于半可判定问题，但Z3对常见的多项式约束（尤其是二次约束）都能给出确定的sat/unsat结果，优化问题也能找到精准的最优解。不过如果约束涉及超越函数（比如sin、exp这类非多项式函数），Z3就无法保证完备性了。

• 非线性整数算术：很遗憾，整数上的非线性算术是不可判定的——不存在任何通用算法能解决所有这类问题。所以Z3对非线性整数约束的处理是启发式的，没有所谓“完备的断言类别”。遇到复杂的非线性整数约束（比如二次优化问题），Z3经常会返回unknown，因为它找不到有效的推理路径来确定结果。

2. 为什么你的二次整数优化代码返回unknown？ #

先看你给出的代码：

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

问题核心在于整数类型的二次优化：

• 手动分析的话，你要最小化的H² - H是整数域上的二次函数，当H >= 1时，这个函数是单调递增的（导数2H-1为正），所以在H ∈ [8000, 12000]的整数范围内，最小值肯定出现在H=8000。
• 但Z3的整数非线性求解器是启发式的，没有完备的算法来处理这类整数二次优化问题。它无法自动识别函数的单调性，也找不到有效的推理路径来确定最优解，因此返回unknown，并标注incomplete (theory arithmetic)——意思是算术理论的求解器不完备，无法处理当前问题。

可行的解决办法： #

• 如果业务场景允许变量用实数类型，把Int换成Real，Z3的非线性实数求解器可以轻松处理这个二次优化问题，返回确定的最优解：

  (declare-fun H () Real)
  (assert (>= H 8000.0))
  (assert (<= H 12000.0))
  (minimize (- (^ H 2) H))
  (check-sat)
  (get-model)
  

  运行后会直接给出H=8000.0的最优解。
• 如果必须用整数类型，你可以手动利用函数的单调性，直接断言H=8000来验证结果，或者通过其他逻辑简化问题（不过二次整数约束没法转成线性约束，只能靠手动推导）。

内容的提问来源于stack exchange，提问作者Jean Chen