z3 - 有人可以帮助在 SMT 求解器 Z3 中对这个函数（多项式函数）进行建模吗？

Question

F(x1) > a;

F(x2) < b;

∀t, F'(x) >= 0 (导数) ;

F(x) = ∑ci*x^i; (i∈[0,n] ; c 是一个常数)

Answer 1

您的问题非常模棱两可，如果您展示您尝试过的内容以及遇到的问题，stack-overflow 效果最好。

不过，这里是如何F = 2x^3 + 3x + 4使用 Python 到 z3 的接口为特定函数编写问题的方法：

from z3 import *

# Represent F as a function. Here we have 2x^3 + 3x + 4
def F(x):
  return 2*x*x*x + 3*x + 4

# Similarly, derivative of F: 6x^2 + 3
def dF(x):
  return 6*x*x + 3

x1, x2, a, b = Ints('x1 x2 a b')
s = Solver()

s.add(F(x1) > a)
s.add(F(x2) < b)

t = Int('t')
s.add(ForAll([t], dF(t) >= 0))

r = s.check()
if r == sat:
    print s.model()
else:
    print ("Solver said: %s" % r)

请注意，我将您的∀t, F'(x) >= 0条件翻译为∀t. F'(t) >= 0. 我假设您在绑定变量中有错字。

当我运行它时，我得到：

[x1 = 0, x2 = 0, b = 5, a = 3]

这种方法可以以明显的方式推广到具有常数系数的任意多项式，但这主要是关于编程而不是 z3。（请注意，在 SMTLib 中这样做要困难得多。这就是 Python 等宿主语言的功能发挥作用的地方。）

请注意，这个问题本质上是非线性的。（变量与变量相乘。）因此，SMT 求解器可能不是这里的最佳选择，因为它们不能很好地处理非线性运算。但是您可以在以后出现这些问题时对其进行处理。希望这能让你开始！