Control whether to use incremental or "bulk" SAT solver

[GSPP]

Apparently, Z3 has multiple SAT solvers. There's an incremental one that is more efficient for push/pop scenarios and there is a "bulk" solver that is more efficient to solve a problem just once.

It is not quite clear to me which one is picked under what circumstances. What exactly triggers what solver to be used?

Can we control the solver to be used? That would be useful because we could empirically test which one performs better for the particular problems that are posed. If this is not possible right now I would like to request this as a feature.

[wintersteiger]

Z3 has tactics that are constructed from more basic elements (both sat solvers being such) and they will be selected based on what appears in your problems, usually by simple features, as the newer SAT solver doesn't support some features that the old one does support, but the old SMT solver does support everything (including SAT). For example, for QF_BV problems it runs the qfbv tactic, which will select the sat tactic (often fast) or the smt tactic (often slow, but supports uninterpreted functions). If there is anything in the problem that's not in QF_BV, then the mk_is_qfbv_probe() will detect that and run the fully-featured SMT solver instead of the pure SAT solver.

If you want full control, you can build such tactics by yourself, either directly in an SMT2 file, or via the API, see the strategies tutorial. There is no option for switching between those two solvers, because the choice between them is usually made based on feature support and not based on performance considerations.

[GSPP]

Is there a way to diagnose what solver has been used and what decisions have been made by the probes?

[wintersteiger]

Yes, run z3.ex3 with -v:10, then it will show which tactics are being executed. You'll see lines starting with (sat-, for instance

(sat-restart :conflicts 11347 :decisions 32414 :restarts 46 :clauses 9221 :learned 10368 :gc-clause 0 :memory 28.04 :time 2.25)

when it uses the pure/new SAT solver, while you will see lines starting with (smt. if the old/slow/fully featured SMT solver is used, for instance

(smt.searching)

[GSPP]

I forgot to mention that I'm using the managed API. Sorry about that. I assume that the statistics object will also show this data?

[wintersteiger]

No, the statistics module has nothing to do with any of that. You can try setting the verbose option to enable the output for the console.

If you feel adventurous, you can also compile Z3 in debug mode and enable managed code debugging in VS, then you can interrupt the execution and see what it is actually doing.

[GSPP]

OK, thanks for answering my questions.

I would like to propose two features:

• Make it easy to find out what solvers took part in solving the problem. This insight should enable developers to optimize their Z3 usage.
• Start documenting optimization strategies for Z3. The document should state how to reliably trigger the fast SAT solver. Also, for example I found that forcing the QF_BV logic increased perf like 3x. I stumbled upon this by accident. I think customers would very much appreciate a list of common optimizations like this one.

[wintersteiger]

These are not "optimzations" in the sense that you require; there is no guarantee that any of this will make things faster for everybody. If you don't specify any logic, Z3 will often run the slowest possible solver because it has to expect anything; this is the whole reason for "logics" being in the SMT standard.

You can see what tactics are being run on the command line. Did setting the verbosity in your API application produce the desired output? You can reliably trigger the "fast" new sat solver by using th "sat" tactic, like I said before.