CODEWITHSUNDEEP
z3satisfiability
Axel Kemper
Axel Kemper

Reputation: 11322

Random seed for Z3 SAT Solver

I am using Z3 as SAT solver for a tough satisfiability problem encoded in CNF/DIMACS format.

Would it make sense to randomize the input in order to increase the chance to find a solution:

Measurements (100 test runs per solver and sorting mode) for a smaller problem with Z3, Cryptominisat and Clasp:

enter image description here

For Z3, sorting/randomization does not look promising for my example which is probably not representative.

I have not found a random seed commandline parameter which influences the SAT module of Z3. Parameter "random_seed" only seems to control the SMT solver.

Upvotes: 2

Views: 899

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

You make an excellent point: the random seed used by the sat solver is not exposed in the same way as the other modules. I have updated the unstable branch with an update to the parameters to the sat solver. You can now set the random seed from the command line as part of the sat parameters. I hope this helps.

Upvotes: 2

Related Questions