How to get random results from Microsoft Z3?

问题:

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.

回答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.

回答2:

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)));
}