Is it possible to ask Z3 to prove satisfiability of a system of integer polynomial inequalities with 2 different variables (or in general case) by approximating the original system with a system of linear inequalities?
可以将文章内容翻译成中文,广告屏蔽插件可能会导致该功能失效(如失效，请关闭广告屏蔽插件后再试):
问题:
回答1:
By default, Z3 will try to solve a nonlinear integer problem as a linear one. The basic trick is to treat nonlinear terms such as x*y as new "variables". Nonlinear integer arithmetic is not well supported in Z3, the following post has a summary on how Z3 handles nonlinear integer arithmetic:
- How does Z3 handle non-linear integer arithmetic?
