Getting a “good” unsat-core with z3 (logic QF_BV)

Question

I am using the Z3 SMT solver to solve a problem that I have expressed in the logic QF_BV, using the SMTLIB 2 language.

The model is unsatisfiable, and I am trying to get the solver to produce an unsat-core.

My model consists of several 'mandatory' constraints, which I specify using assert statements.

The assertions that I want to be considered for unsat-core generation, have been specified using the (assert (! (EXPR) :named NAME)) construct.

Z3 gives me an unsat, as expected. However, Z3 always seems to dump a 'trivial' unsat-core consisting of ALL the named assertions.

I know that there exists a subset of my named assertions, which is an unsat-core. I found this core using Yices SMT solver, which frequently gives me relatively smaller unsat-cores. The Yices model is the same as the Z3 model (pretty much a line-by-line translation from SMT2 to the Yices input language).

Is producing "good" unsat-cores a solver-specific feature, or are there any generic suggestions/changes I could make to help Z3 give me a better core?

Answer 1

Z3 and Yices 1.x use the same approach for computing unsat cores. The track all assertions that were used in the proof of unsatisfiability. However, the proofs built by each system may be quite different. There are algorithms for computing minimal unsat cores on top of the capabilities provided by Z3 and Yices. Here is a reference.

EDIT: by default, Z3 uses several pre-processing steps before it tries to solve a problem. Some of these steps may affect the generation of the unsat core. In particular, it eliminates constants using the equations in the problem. We say Z3 "solves" the equations and eliminate the variables. In your script, you can get a smaller core by disabling this step. We can accomplish that by using the option

(set-option :auto-config false)

Z3 will execute a very general configuration. For bit-vector problems it is usually a good idea to disable "relevacy propagation":

(set-option :relevancy 0)

Finally, we can now enable/disable the variable elimination step, and see the effect on the unsat core size.

(set-option :solver true) ;; Z3 will generate the core C0 C1 C2
(set-option :solver false) ;; Z3 will generate the core C1 C2