我想知道是否有可能解决具有多项式约束的优化问题?我特别想知道关于Z3。
在Z3教程中，它说它支持多项式约束，但我不知道这是否适用于优化，或者如果这只是为了约束解决。
非常感谢，所有的回答都非常感谢。
汤姆
形式x^n + x^(n-1) + ... + c = k的约束引入了非线性项。(两个变量相乘;在这种情况下是同一个。)z3的优化器不处理非线性约束。详见https://stackoverflow.com/a/50319193/936310