Modifying the divide and conquer SAT search in Z3-Python

Question

I am trying to modify the divide and conquer SAT search in Z3 (Python), but feel completely lost. I will explain my question in three parts.

Introduction

I am performing a SAT search loop in Z3 using its default incremental options (i.e. using add).

However, I was made aware that my search is a simple enumeration of type "find me all-solutions", which consists on "add the negation of the previous model and iterate". Like the following:

  ...
  phi = a_formula
  s = Solver()
  s.add(phi)
  while  s.check() == sat: 
    s.check()
    m = s.model()
    phi = add_modelNegation(m)
    s.add(phi) #in order not to explore the same model again
  ...

This is clearly a 'brute-force' implementation.

Also I was noted that, instead of it, I could use a "divide-and-conquer" approach, in order to make the search faster. To do so, I was offered the following link (Z3Py) checking all solutions for equation (see the last answer by @alias). I tested this code works at In Z3-Python, I get "builtin_function_or_method' object is not iterable" when performing model search. The code is essentially the following:

def all_smt(s, initial_terms):
    def block_term(s, m, t):
        s.add(t != m.eval(t, model_completion=True))
    def fix_term(s, m, t):
        s.add(t == m.eval(t, model_completion=True))
    def all_smt_rec(terms):
        if sat == s.check():
           m = s.model()
           yield m
           for i in range(len(terms)):
               s.push()
               block_term(s, m, terms[i])
               for j in range(i):
                   fix_term(s, m, terms[j])
               yield from all_smt_rec(terms[i:])
               s.pop()   
    yield from all_smt_rec(list(initial_terms))

The problem

My SAT problem is not that 'basic' one in which I just enumerate (or rapidly enumerate, if I follow the code above) all solutions. I have a 'booster' that allows me to add more restrictions if a given model holds some properties. This booster is a kind of heuristic. The schema is as follows:

  ...
  s = Solver()
  s.add(True)
  while  s.check() == sat: 
    s.check()
    m = s.model()
    phi = add_modelNegation(m)
    s.add(phi) #in order not to explore the same model again
    if holds_property(m): #if the model holds a property
       add_moreConstraints(s,m) #add other constrains to the formula
  ...

I would like to add the all_smt ideas to this version, accurately making use of push and pop. My problem is that I do not perfectly understand the usage of push and pop and, since my code does not fix variables like the fast one does, I do not not how to 'merge' both ideas. How can I adapt my code to be faster?

A concrete coding example:

I offer a concrete example below. This is an example made in order to facilitate your coding, but it makes no sense in reality.

For instance, imagine that the booster or heuristic is that if the number of False assignments in the model is greater than 1, then we can add the 'reversed' model to the solver, where the 'reversed' model just changes the value of each assignment to the opposite. For instance, if the model is phi=[c0=True, c1=False, c2=False, c3=True], then phi holds the property and, thus, its 'reverse' is added, where phi_reversed = [c0=False, c1=True, c2=True, c3=False]. On the other side, phi'=[c0=True, c1=True, c2=False, c3=True] does not hold the property, so nothing additional is added to the solver.

I repeat that this booster makes no sense, but it is enough for the sake of coding. So let us make that function:

def holds_property(m, varss):
    numFalses = 0
    for x in varss:
       if m[x] == False:
         numFalses = numFalses + 1
    if numFalses > 1:
       return True
    else:
       return False

And also the function that creates the 'reversed' version of a model:

def make_reverse(m, varss):
    for x in varss:
       if m[x] == True:
          m[x] = False
       elif m[x] == False:
          m[x] = True
    return m

I will also invent a formula and a set of variables. Thus, my 'brute-force' implementation is (this is not pseudo-code):

  a,b,c = Bools('a b 'c)
  varss = [a,b,c]
  phi = And(a, Or(b,c))
  s = Solver()
  s.add(phi)
  models = []
  while  s.check() == sat: 
    s.check()
    m = s.model()
    models.append(m)
    phi = add_modelNegation(m)
    s.add(phi)
    if holds_property(m, varss):
       s.add(make_reverse(m, varss))
  return models

The question is, again: how can I insert (or modify) the ideas of the 'fast' version to this one? I would like to add 'fixing' with push and pop, basically.

Any help? I know the question is dense but tried to explain it calmly and with examples :) Anyway, do not hesitate to ask more and I will edit the post.

Answer 1

When you push, you're creating a nesting level in your assertions. That is, the solver puts a marker on the assertion stack, which you can jump back to later on with a call to pop. What this means, of course, is that when you do the pop, you'll lose all the assertions that you inserted after the last push.

Since you have extra constraints, simply keep track of them, and manage them between calls to push and pop. Something like this:

from z3 import *

def pruned_all_smt(s, initial_terms, holds_property, more_constraints):

    global extra_constraints

    extra_constraints = []

    def block_term(m, t):
        s.add(t != m.eval(t, model_completion=True))

    def fix_term(m, t):
        s.add(t == m.eval(t, model_completion=True))

    def custom_pop():
        global extra_constraints

        s.pop()
        for ec in extra_constraints:
            s.add(ec)

    def custom_model():
        global extra_constraints

        m = s.model()

        if holds_property(m):
            extra_constraints = more_constraints(m) + extra_constraints

        for ec in extra_constraints:
            s.add(ec)

        return m

    def pruned_all_smt_rec(terms):
        if sat == s.check():
           m = custom_model()
           yield m
           for i in range(len(terms)):
               s.push()
               block_term(m, terms[i])
               for j in range(i):
                   fix_term(m, terms[j])
               yield from pruned_all_smt_rec(terms[i:])
               custom_pop()

    yield from pruned_all_smt_rec(list(initial_terms))

Note that we made the the hold_property and more_constraint parameters, so you need to supply those separately. Here's a template use:

def check_prop(m):
    return True;

def more_constraints(m):
    return []

Given this, you'd use it as:

print(list(pruned_all_smt(s, varss, check_prop, more_constraints)))

Give this a try and see how far it takes you. I haven't really tested this with anything meaningful, so there might be some gotchas!