有人可以帮助在SMT求解器Z3中对该函数多项式函数建模吗？

问题描述

F（x1）> a;

F（x2）

∀t，F'（x）> = 0（导数）;

（p）F（x）= ∑ ci * x ^ i; （i∈[0，n]; c是一个常数）

解决方法

您的问题非常模棱两可，如果您展示自己尝试过的内容和遇到的问题，则堆栈溢出的效果最佳。

不过，以下是使用z3的Python接口可以为特定功能F = 2x^3 + 3x + 4编写问题的方法：

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求解器可能不是最佳选择，因为它们不能很好地处理非线性运算。但是您可以处理以后出现的那些问题。希望这可以帮助您入门！

smt z3 z3py