Z3 randomness of generated model values

Question

I'm trying to influence the randomness of results for model values generated by Z3. As far as I understand, the options for this are very limited: in case of linear arithmetic, the simplex solver does not allow for random results that still satisfy the given constraints. However, there is an option smt.arith.random_initial_value ("use random initial values in the simplex-based procedure for linear arithmetic (default: false)") which I don't seem to get working:

from z3 import *
set_option('smt.arith.random_initial_value',True)
x = Int('x')
y = Int('y')
s = Solver()
s.add( x+y > 0)
s.check()
s.model()

This seems to always produce [y = 0, x = 1] as a result. Even model completion for variables unused in the given constraints seems to produce deterministic results all the time.

Any ideas or hints about how this option works?

Cultivator

Would you be interested in an iterative way to achieve kind of random models? You could refine a given model by adding random constraints like x >= rand() until you get unsat. – Septa

Answer 1

Thanks for catching that! There was indeed a bug that caused the random seed not to be passed through to the arithmetic theory. This is now fixed in the unstable branch (fix here).

This example:

(set-option :smt.arith.random_initial_value true)
(declare-const x Int)
(declare-const y Int)
(assert (> (+ x y) 0))
(check-sat-using (using-params qflra :random_seed 1))
(get-model)
(check-sat-using (using-params qflra :random_seed 2))
(get-model)
(check-sat-using (using-params qflra :random_seed 3))
(get-model)

Now produces three different models:

sat
model
  (define-fun y () Int
    4294966763)
  (define-fun x () Int
    4294966337)
)
sat
(model
  (define-fun y () Int
    216)
  (define-fun x () Int
    4294966341)
)
sat
(model
  (define-fun y () Int
    196)
  (define-fun x () Int
    4294966344)
)

It looks like there may be another place where this option isn't passed through correctly (e.g., when using set-logic instead of calling the qflra tactic directly), we're still looking into that.

Renown

How can I specify check-sat-using (using-params qflra :random_seed 2) in python when using z3py? I looked everywhere and could not find it... I could only find the equivalent of the check-sat, which is just solver.check(). – Demagogue