Satisfiablity checking in non-linear integer arithmetic by approximation

Question

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?

score 1 · Answer 1 · edited May 23 '17 at 12:12

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?

edited May 23 '17 at 12:12

Community

1
1

answered Dec 27 '12 at 16:40

Leonardo de Moura

21,065
2
47
53

Satisfiablity checking in non-linear integer arithmetic by approximation

1 Answers1

Linked