CODEWITHSUNDEEP
z3smt
Tom
Tom

Reputation: 934

Why Z3 always return unknown when assertions have power?

Here is the input

Example 1

(declare-var a Int)
(declare-var b Int)
(declare-var n Int)
(assert (= b (* a a)))
(assert (not (= b (^ a 2))))
(check-sat)

Example 2

(declare-var a Int)
(declare-var b Int)
(declare-var n Int)
(assert (= b (* (^ a n) a)))
(assert (not (= b (^ a (+ n 1)))))
(check-sat)

It returns unknown almost instantaneously.

Upvotes: 1

Views: 654

Answers (1)

alias
alias

Reputation: 30525

Your problem falls into the fragment known as non-linear integer arithmetic, which is undecidable. That is, there is no decision procedure to determine the satisfiability of your query. (Non-linear means, basically, there is a multiplicative term involving at least two variables.)

Having said that, most solvers do have heuristics to answer queries involving non-linear arithmetic, and Z3 is no exception. Of course, being a heuristic, it may or may not produce an answer. This is what you are observing, alas it appears the default tactics Z3 uses is just not sufficient for your problems.

As a common trick, you can try Z3's non-linear real-arithmetic solver for these sorts of problems. Instead of check-sat, use:

(check-sat-using qfnra-nlsat)

In this case, Z3 tries to solve the benchmark assuming the inputs are reals, and sees if the solution is actually integer. This trick can successfully resolve some integer-nonlinear arithmetic queries, though of course not always. For instance, if you try qfnra-nlsat on your first example you'll see that it successfully solves it, but it still answers unknown for the second one.

For details on non-linear integer arithmetic and Z3, see here: How does Z3 handle non-linear integer arithmetic?

Upvotes: 3

Related Questions