CODEWITHSUNDEEP
z3
Cristian Petrescu-Prahova
Cristian Petrescu-Prahova

Reputation: 157

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

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)

Upvotes: 1

Views: 343

Answers (1)

iago
iago

Reputation: 277

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:

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

Upvotes: 1

Related Questions