What is the difference between Z3_solver_check() and Z3_solver_check_assumptions()?

[delcypher]

Aside from the fact that their interfaces are different and that Z3_solver_check_assumptions() doesn't modify the solver's assertion stack (thus avoiding use of push/pop) are these functions expected to perform differently in anyway?

Personally I'm wondering if Z3 is expected perform better if the "assumptions" provided are satisfiable? This seems to hinted at on this old SMTLIB mailing list post but I'm wondering if this really is the case for Z3.

[NikolajBjorner]

check-assumptions originates with MiniSAT and other SAT solvers where selected literals are pushed on an assertion stack. It is then easy to use the SAT solver conflict mechanism to track if the assumptions are used in conflicts. In the end we can use the assumptions that are in the unsat core to track what subset of assumptions are inconsistent when taken in conjunction with the asserted formulas. Thus, assumptions are used to extract cores. After search completes learned clauses that don't contain the assumptions are thus independent of them and can be reused in the next SAT call. This is different from push/pop where all learned clauses under a push are removed. So even if the assumptions you use in one call are not leading to an answer "unsat" it is possible that the call involves learning some clauses that can remain valid for the next call.

[delcypher]

@NikolajBjorner Thanks for the explanation. Will Z3 do what you describe if Z3's SAT solver gets called?

If I use my own custom tactic (that calls the sat tactic) will this work, or will the problem get solved scratch every time?

[NikolajBjorner]

tactics are not incremental, only solvers have a chance to be. If you create a solver from a tactic, the resulting solver just calls the tactic from scratch every time.

[delcypher]

tactics are not incremental, only solvers have a chance to be. If you create a solver from a tactic, the resulting solver just calls the tactic from scratch every time.

Okay. So I would need to create the solver via Z3_mk_solver_for_logic() (where logic is QF_BV for example) to get this incremental behaviour when using the sat solver?

Looking at the current implementation Z3_mk_solver_for_logic() calls mk_smt_strategic_solver_factory(symbol const & logic) which makes a combined solver where the second solver comes from mk_smt_strategic_solver_factory(symbol const & logic) which under the right conditions (logic is QF_BV and rw.hi_div0() is true) calls mk_inc_sat_solver(m, p). Presumably mk_inc_sat_solver(m, p) is the solver I'm looking for (although I'm surprised it is used for QF_BV directly, I would have thought bit-blasting would need to be done somewhere).

If that is the case then there are quite a few hoops to jump through to get at the incremental SAT solver

• Logic must be QF_BV (reasonable restriction)
• Must configure combined solver to not use the first solver at all (not the default)
• hi_div0 must be true (appears to be the default)

Is that correct?

[wintersteiger]

Yep, that looks like the only combination of facts that gets you the new SAT solver with incremental features. Bit-blasting is done in the preprocessing stage of the inc_sat_solver by using a tactic, i.e., this will not be incremental as far as I can tell (code looks sound, but will waste time/memory).

@NikolajBjorner I think we should make it easier to get at that. Those questions/requests will come up more than once. Maybe Z3_mk_solver_for_logic("SAT")? Given that we also have Z3_mk_simple_solver(), we might as well add a whole new Z3_mk_sat_solver().

[delcypher]

I would vote Z3_mk_sat_solver() but that's just because it's not obvious what the "SAT" logic is (I wouldn't have guessed that it is QF_BV based on the name) and currently it isn't documented (AFAIK) what logic names are supported so nobody will be able to easily discovered there is a logic named "SAT".

[NikolajBjorner]

There is Z3_mk_solver_for("QF_FD") and Z3_mk_solver_for("QF_BV") already.

[wintersteiger]

Yes, in theory everything is possible! In practice, Z3_mk_solver_for("QF_BV") will construct either a 'simple' solver, a 'combined/strategic solver', or a SAT solver, depending on parameter settings and the contents of the goal later, and most of this is undocumented. I'm just saying... I think that's one too many hoops we ask the users to jump through.

@delcypher : we tend to support the official SMT logics, so "SAT" would break that convention. But, we recently added "ALL" too... This gives you a good idea of what magic strings Z3 recognizes as logic names. It's not really worth fixing or even documenting though, because the whole idea of logic names is flawed and the SMT community is currently working out a solution. Ideally, Z3 should work without specifying a logic, as it will figure out what it needs and where it can cut corners (but that doesn't always work either...).

[NikolajBjorner]

Can this be closed now?

[delcypher]

@NikolajBjorner No. Although the question was answered the issue relating to access to the incremental sat solver remains unresolved (maybe a separate issue should be opened for that?).

I noticed in 97e2632 you made SAT an alias for QF_FD. I don't understand this change at all.
What does QF_FD stand for (quantifier free ???) ? I thought the point of what @wintersteiger proposed was for the SAT "logic" to use mk_inc_sat_solver() not mk_fd_solver()

[NikolajBjorner]

Fd is for finite domains. It uses incsatsolver, otherwise compiles away enumeration, finite range integers and bitvectors. I see no internal motivation to maintain a separate solver.

[NikolajBjorner]

issue relating to access to the incremental sat solver remains unresolved

The answer is to use Z3_mk_solver_for("QF_FD"). Given that this option is by now somewhat mature, I will close this issue