How does Z3 handle non-linear integer arithmetic?
Solution 1:
Yes, the decision problem for nonlinear integer arithmetic is undecidable. We can encode the Halting problem for Turing machines in nonlinear integer arithmetic. I strongly recommend the beautiful book Hilbert's tenth problem for anybody interested in this problem.
Note that, if a formula has a solution, we can always find it by brute force. That is, we keep enumerating all possible assignments, and testing whether they satisfy the formula or not. This is not that different from trying to solve the Halting problem by just running the program and checking whether it terminates after a given number of steps.
Z3 does not perform a naive enumeration. Given a number k, it encodes every integer variable using k bits and reduces everything into Propositional logic. Then, a SAT solver is used to find a solution. If a solution is found, it converts it back into an integer solution for the original formula. If there is no solution for the Propositional formal, then it tries to increase k, or switches to a different strategy. This reduction to Propositional logic is essentially a model/solution finding procedure. It can't show that a problem does not have a solution. Actually, for problems where every integer variable has a lower and upper bound, it can do it. So, Z3 has to use other strategies for showing no solution exists.
Moreover, the reduction into Propositional logic only works if there is a very small solution (a solution that needs a small number of bits to be encoded). I discuss that in the following post:
- Need help understanding the equation
Z3 does not have good support for nonlinear integer arithmetic. The approach described above is very simplistic. In my opinion, Mathematica seems to have the most comprehensive portfolio of techniques:
http://reference.wolfram.com/legacy/v5_2/functions/AdvancedDocumentationDiophantinePolynomialSystems
Finally, the nonlinear real arithmetic (NLSat) solver is not used by default for nonlinear integer problems. It is usually very ineffective on integer problems. Nonetheless, we can force Z3 to use NLSat even for integer problems. We just have to replace:
(check-sat)
With
(check-sat-using qfnra-nlsat)
When this command is used, Z3 will solve the problem as a real problem. If no real solution is found, we know there is no integer solution. If a solution is found, Z3 will check if the solution is really assigning integer values to integer variables. If that is not the case, it will return unknown to indicate it failed to solve the problem.