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

Question

I use the Z3 SMT solver to solve the problem that I expressed in the QF_BV logic using the SMTLIB 2 language.

The model is unsatisfactory, and I'm trying to get the solver to create unsat-core.

My model consists of several mandatory restrictions that I specify using assert .

The statements that I want to consider for generating unsaturated kernels have been defined using the construct (assert (! (EXPR) :named NAME)) .

Z3 gives me unsat , as expected. However, Z3 always seems to discard the “trivial” unsat-core, consisting of ALL of these statements.

I know that there is a subset of my named statements, which is unsat-core. I found this kernel using the Yices SMT solver, which often gives me relatively small unsat-core. The Yices model is the same as the Z3 model (basically line by line feed from SMT2 to Yices input language).

Does it produce "good" solver-dependent unsat-core functions, or are there any general suggestions / changes I could make to help Z3 give me a better kernel?

Answer 1

Z3 and Yices 1.x use the same approach to calculate unsaturated cores. Track all statements that were used to prove unsatisfactory. However, the evidence built by each system can be completely different. Algorithms exist for calculating the minimum unsaturated cores on top of the capabilities provided by Z3 and Yices. Here's a link .

EDIT: By default, Z3 uses several preprocessing steps before trying to solve the problem. Some of these steps can affect the generation of an unsaturated core. In particular, it removes the constants using equations in the problem. We say that Z3 "solves" equations and excludes variables. In a script, you can get a smaller kernel by disabling this step. We can do this using the option

 (set-option :auto-config false) 

Z3 will perform a very general configuration. For tasks with bit vectors, it is usually recommended to disable “relevance propagation”:

 (set-option :relevancy 0) 

Finally, now we can enable / disable the step of excluding variables and see the effect on the size of the inactive kernel.

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