6

In Microsoft Z3, when we try to solve a formula, Z3 always returns the results in the same sequence, when there are two or more satisfiable solutions.

Is it possible to get random results from Z3 so that for the same input, it will generate different output sequence in different execution.

Please note that, I am using C or C# API. I am not using Z3 using smt2lib. So if you can give me a C or C# API function example that can add randomization, it will be more useful.

Amarjit Datta
  • 251
  • 2
  • 7

2 Answers2

1
(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)

Taken from here.

Community
  • 1
  • 1
mmpourhashem
  • 91
  • 1
  • 6
  • What language is this? Looks Scheme-y – Carcigenicate Feb 12 '16 at 18:56
  • 1
    It's smt2, normal input of Z3 without any API. Check this out rise4fun.com/Z3 . – mmpourhashem Feb 12 '16 at 23:03
  • I tried above parameters using C API code ... cfg = Z3_mk_config(); Z3_set_param_value(cfg, "MODEL", "true"); Z3_set_param_value(cfg, "TIMEOUT", TIME_OUT); Z3_set_param_value(cfg, "SMT.ARITH.RANDOM_INITIAL_VALUE", "true"); Z3_set_param_value(cfg, "RANDOM_SEED", "1"); solver = Z3_mk_context(cfg); ... Unfortunately I couldn't make it work. When I run the code, I get warning like this... WARNING: unknown parameter 'smt.arith.random_initial_value' WARNING: unknown parameter 'random_seed' Any idea where I have done wrong? – Amarjit Datta Feb 15 '16 at 06:01
0

You can write a while loop to find all the solutions, and if you want them randomly, what you can do is write one simple constraint that will hide (in real-world 'negate') the solution it has got previously. Like:

int numSolution = 0;
while (true)
{
 do something;.....
 BoolExpr[] args = new BoolExpr[];
 args[i] = your solution variable;
 numSolution++;
 if (numSolution == MAX_NUM_SOLUTION)
  {               
    break;
   }                
 slvr.Assert(z3.MkNot(z3.MkAnd(args)));
}
Rahat
  • 16
  • 2