Different run times for the same constraint set using Z3Py

1
votes

I'm encoding a scheduling problem with the Z3 solver using the z3py API. It works pretty well apart from the fact that the runtimes of the solver differs in time (sometimes by factor 10/100) in each run. What I often do if the solver takes too long, I just kill the query and restart it.

It seems to me that the solver (for each run) takes a somehow different path to find a solution, which results in different run times.

So my question is, whether I can force a solver to take the same(similar) path every time for the same set of constraints (problem)?

After doing some research I stumbled upon the concept of setting a random seed manually. Would that help me? Is there any more info how to do that with the python api?

best

Jenny

1
pythonz3z3py

1 Answers

1
votes

Not unless you know ahead of time which random seed works the best. However, you can indeed set the seed in regression scenarios, to get repeatable behavior.

Inspecting the output of z3 -p, I see many possibilities:

fixedpoint.spacer.random_seed (unsigned int) (default: 0)
sat.random_seed (unsigned int) (default: 0)
nlsat.seed (unsigned int) (default: 0)
fp.spacer.random_seed (unsigned int) (default: 0)
smt.random_seed (unsigned int) (default: 0)
sls.random_seed (unsigned int) (default: 0)

(NB. 0 tells "pick" it yourself to the solver.) The one you want is most likely smt. or sat. one; perhaps both.

You can set this option from the Python API, using the set_param function, see: https://z3prover.github.io/api/html/namespacez3py.html#a54767807c828563030b9400332f81d48