partial assignments in Z3

Question

I have a Boolean formula (format: CNF) whose satisfiablity I check using the Z3 SAT solver. I am interested in obtaining partial assignments when the formula is satisfiable. I tried model.partial=true on a simple formula for an OR gate and did not get any partial assignment.

Can you suggest how this can be done? I have no constraints on the assignment other than that it be partial.

Answer 1

Z3's partial model mode are just for models of functions. For propositional formulas there is no assurance that models use a minimal number of assignments. On the contrary, the default mode of SAT solvers is that they find complete assignments.

Suppose you are interested in a minimized number of literals, such that the conjunction of the literals imply the formula. You can use unsat cores to get such subsets. The idea is that you first find a model of your formula F as a conjunction of literals l1, l2, ..., ln. Then given that this is a model of F we have that l1 & l2 & ... & ln & not F is unsatisfiable. So the idea is to assert "not F" and check satisfiability of "not F" modulo assumptions l1, l2, .., ln. Since the result is unsat, you can query Z3 to retrieve an unsat core among l1, l2, .., ln.

From python what you would do is to create two solver objects:

    s1 = Solver()
    s2 = Solver()

Then you add F, respectively, Not(F):

    s1.add(F)
    s2.add(Not(F))

then you find a reduced model for F using both solvers:

    is_Sat = s1.check()
    if is_Sat != sat:
       # do something else, return
    m = s1.model()
    literals = [sign(m, m[idx]()) for idx in range(len(m)) ]
    is_sat = s2.check(literals)
    if is_Sat != unsat:
       # should not happen
    core = s2.unsat_core()
    print core

where

    def sign(m, c):
        val = m.eval(c)
        if is_true(val):
           return c
        else if is_false(val):
           return Not(c)
        else:
           # should not happen for propositional variables.
           return BoolVal(True)

There are of course other ways to get reduced set of literals. A partial cheap way is to eagerly evaluate each clause and add literals from the model until each clause is satisfied by at least one literal in the model. In other words, you are looking for a minimal hitting set. You would have to implement this outside of Z3.