35

I am aware that the theory of integers with multiplication is generically undecidable. Nevertheless, in certain instances, Z3 does return a model. I am curious to know how this is done. Does it have something to do with the new decision procedure for non-linear arithmetic over reals? What specific instances (eg: Integers under finite modulus etc) have been recognized for which Z3 returns a model for a multiplication query? Any help is much appreciated.

1
  • 14
    This is a valid question. Please do not down vote it, or vote to close it. Thanks. Dec 16, 2012 at 4:13

1 Answer 1

38

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:

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.

0

Your Answer

Reminder: Answers generated by Artificial Intelligence tools are not allowed on Stack Overflow. Learn more

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.