Can't explain how a simple tweak leads to "unknown" Z3 result

Question

I'm learning Z3. I was working with some simple "isPrime" function and stumbled upon some hard to understand behavior. A seemingly "simpler" inlined formula, (> q 1), leads to "unknown", versus a more "complex" define-fun (macro), (isPrime q), leads to a quick solution, even as (isPrime q) subsumes (> q 1). http://rise4fun.com/Z3/slg2D.

(define-fun isPrime ((x Int)) Bool
  (and (> x 1) (not (exists ((z Int) (y Int)) (and (not (= y x)) (and (not (= z x)) (and (> y 1) (> z 1) (= x (* y z)))))))))
(declare-const q Int)
(declare-const r Int)
(assert (and
  ;with this the '+ 2' variation is sat: 5, 3
  ;(isPrime q)
  (> q 1)
  (> r 1)
  ;always answers sat: 2, 2
  ;(isPrime (+ (* q r) 1))
  ;unknown
  (isPrime (+ (* q r) 2))
))
(check-sat)
(get-model)

Which one is the _simpler inlined formula_? Could you state the question more clearly? — iago, Feb 29 '16 at 09:14
```(isPrime q)``` => sat. ```(> q 1)``` => unknown. ```(> q 1)``` is subsumed by ```(isPrime q)```. — Cristian Petrescu-Prahova, Feb 29 '16 at 17:10

iago · Accepted Answer · 2016-02-29T22:02:45.133

Quantified logics is kind of an advanced feature, and you should read about how Z3 solves these formulas, that will give you perspective on what you can expect from Z3. Solving formulas with quantifiers is a delicate art, in my humble experience. Things that are obvious to you, may not be obvious to Z3.

You have a forall quantifier (you wrote it as not exists) that Z3 will try to satisfy. I guess that Z3 is picking some q and r and then checking if isPrime holds, otherwise it tries with a new pair, and so on. If Z3 does not make the right choices it may take a while until it finds such q and r, so maybe you should give it more time (there is a timeout for solving problems on rise4fun).

Another way to proceed could be to help Z3 a bit more. For instance, let it know that z and y are smaller than x. This way you provide a lower and an upper bound for these variables.

(define-fun isPrime ((x Int)) Bool
   (and (> x 1) (not (exists ((z Int) (y Int)) (and (< y x) (and (< z x) (and (> y 1) (> z 1) (= x (* y z)))))))))

This works for me.

update

References:

Leonardo de Moura's talk on the SAT/SMT Summer School 2012 (https://es-static.fbk.eu/events/satsmtschool12/)
Z3 Tutorial, Quantifiers (http://rise4fun.com/Z3/tutorial/guide)
Universal Z3 Tutorial (http://research.microsoft.com/en-us/um/redmond/projects/z3/mbqi-tutorial/main.html)

Thanks for the response. I'm new to Z3, I don't have yet a good sense of how to debug it or what to read. Do you have a specific pointer for Z3 and quantifier formulas? — Cristian Petrescu-Prahova, Feb 29 '16 at 17:16
I have updated my answer with some references I have queried in the past. — iago, Feb 29 '16 at 22:03
You should also check out other related questions/answers, such as http://stackoverflow.com/questions/13268394/avoiding-quantifiers-in-z3. — iago, Feb 29 '16 at 22:05

Can't explain how a simple tweak leads to "unknown" Z3 result

1 Answers1