[SOLVED] Z3-Python as SAT solver does not give right results

Z3-Python as SAT solver does not give right results

I am trying to use Z3 (in Python) as a SAT solver, but the results are unexpected.

First, imagine I want to get a model for the following formula:

from z3 import *

c_0 = Bool('c_0')
c_1 = Bool('c_1')
c_2 = Bool('c_2')
c_3 = Bool('c_3')

sss = Solver()
negations = And(Not(c_0), Not(c_1), Not(c_2), Not(c_3))
sss.add(Not(negations))
print(sss.check())
print(sss.model())

So I get sat, with the model [c_0 = True, c_3 = False, c_1 = False, c_2 = False], which holds the formula (I do not know why the variable assignments are given in that order).

But now, I add And(Not(c_1), Not(c_2), Not(c_3)) to the formula (no need to understand why). Then I get the result unsat, which makes no sense. The result should be sat, for instance, with the model [c_0 = True, c_1 = False, c_2 = True, c_3 = False].

Here is the code:

added_negations = And(Not(c_1), Not(c_2), Not(c_3))
new_Negations = And(negations, Not(added_negations))

ss = Solver()
ss.add(new_Negations)
print(new_Negations)
print(ss.check())

Any help? I tested this using explicit Exists(c_0,c_1...) but the result is the same.

I MADE A MISTAKE!!!

There is a negation missing in new_Negations = And(negations, Not(added_negations)). Correctly: new_Negations = And(Not(negations), Not(added_negations))

Correcting this, the result is again sat, concretely, with a model: [c_0 = False, c_3 = False, c_1 = True, c_2 = False]

Solution

You created two solvers, one called ss, the other called sss. They’re independent. If you want to add new clauses, just use the existing solver, do not create a new one.