Change z3 behavior on demand for unsaturated core

Question

I have some examples of SMTLIB2 that z3 usually finds unsat in 10 s, however when I add unsaturated kernels to the request, check-sat continues to work for several minutes without returning. Is this behavior expected? Does unsat core ask for more than just switching write dependencies to tools and changing which procedures and parameters z3 works with? Is it possible to set additional parameters, so I see the same behavior when I use an inactive kernel, as I see when I do not use it?

I am using Z3 4.3.1 (stable branch) in Scientific Linux 6.3.

Examples are given in AUFNIRA, although some of them do not contain any realities and are probably not non-linear.

Thank,

Pavel.

Answer 1

Unused kernels are tracked using "response literals" (e.g. assumptions). When we enable inactive kernel extracts and uses, such as

(assert (! (= x 10) :named a1)) 

Z3 will internally create a new boolean for the name a1 and claim

 (assert (=> a1 (= x 10))) 

When check-sat is called, it assumes that all of these helper variables are true. That is, Z3 is trying to show that the problem is unsat / sat modulo these assumptions. For feasible examples, it will be completed, as usual, using the model. For unsatisfactory instances, it stops whenever it generates a lemma containing only these alleged Boolean variables. The lemma has the form (or (not a_i1) ... (not a_in)) , where a_i is a subset of the proposed Boolean variables. As far as I know, this technique was introduced by the MiniSAT solver. It is described here (section 3). I really like it because it’s easy to implement, and we are essentially freeing up the base generation for free.

However, this approach has some disadvantages. First, some preprocessing steps no longer apply. If we just say that

 (assert (= x 10)) 

Z3 will replace x with 10 everywhere. We say that the Z3 performs “value distribution.” This preprocessing step does not apply if the assertion is of the form

 (assert (=> a1 (= x 10))) 

This is just an example, many other preprocessing steps affect it. During the solution, some of the simplification steps are also disabled. If we check the Z3 source file smt_context.cpp , we find the code, for example:

  void context::simplify_clauses() { // Remark: when assumptions are used m_scope_lvl >= m_search_lvl > m_base_lvl. Therefore, no simplification is performed. if (m_scope_lvl > m_base_lvl) return; ... } 

The condition m_scope_lvl > m_base_lvl) always true when "response literals" / assumptions are used. Thus, when we include an unreliable base generation, we can really affect performance. It seems that nothing is really free :)