非线性整数算法中的可满足性检验 [英] Satisfiablity checking in non-linear integer arithmetic by approximation

问题描述

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

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?

推荐答案

默认情况下，Z3 将尝试将非线性整数问题作为线性问题求解.基本技巧是将诸如 x*y 之类的非线性项视为新的变量".Z3 没有很好地支持非线性整数运算，以下帖子总结了 Z3 如何处理非线性整数运算:

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:

• Z3 如何处理非线性整数算术?

这篇关于非线性整数算法中的可满足性检验的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！