Z3 and strategies: Which strategy to use?

Question

so I'm trying to solve a scheduling problem using z3. I have a set of jobs which needs to be done and a set of resources that are able to do those jobs. The jobs are ordered (total order) and in general the problem is expressed using linear arithmetic equations (=, <,>) and boolean expressions (e.g: job1 and job2 allocated to different resources => they can run in parallel).

The constraints itself are not complex but the amount of constraints that I'm throwing at the solver is in the thousands and might increase by a factor of 10.

So one of the problems I have is that the Z3 seems to be not deterministic in how it tries to solve the same problem (but during different runs). Sometimes it produces a result within seconds but sometimes it takes time. What I then often do is to kill the current run and restart and then it again gives me a result almost instantaneous. I was wondering, whether using certain strategies/tactics would help to steer Z3 in the right direction more consistently?

I'm using z3py (with optimization) and when I do print(len(z3.tactics())) I see that there are 107 different tactics. And if I print the descriptions for those tactics using print(z3.tactics()) its pretty overwhelming.

Does anyone know a paper/website that basically can give me a hint which tactic to use depending on which kind of constraints I am using? (in my case: linear arithmetic and some boolean constraints without quantifiers)

Answer 1

Z3 tactics are poorly documented, unfortunately. But developers aren't really to blame: tactic-based theorem proving is inherently tied to specifics of an implementation: Whether it's a good old manual prover (Isabelle, HOL, Coq, etc.) or a more modern/automated prover/solver such as Lean/Z3 etc. The best strategy is to keep applying them and see if you can find the right combination. Admittedly this is not the most helpful advice, but at this point picking the right tactic is more of an art than science and requires deep knowledge of the solver itself.

Having said that, there's some rudimentary documentation here: http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/strategies-examples.htm

If you were to experiment and document your findings, I'm sure others following up on z3 would find it useful!