2

是否可以要求 Z3 通过用线性不等式系统逼近原始系统来证明具有 2 个不同变量（或一般情况下）的整数多项式不等式系统的可满足性？

4

1 回答 1

1

默认情况下，Z3 将尝试将非线性整数问题作为线性问题求解。基本技巧是处理非线性项，例如x*y新的“变量”。Z3 不太支持非线性整数运算，下面的帖子总结了 Z3 如何处理非线性整数运算：

于 2012-12-27T16:40:49.750 回答