Z3-Python como solver de SAT no proporciona los resultados correctos.

Estoy tratando de usar Z3 (en Python) como un solucionador SAT, pero los resultados son inesperados.

Primero, imagina que quiero obtener un modelo para la siguiente fórmula:

from z3 import *

c0 = Bool('c0')
c1 = Bool('c1')
c2 = Bool('c2')
c3 = Bool('c3')

sss = Solver()
negations = And(Not(c0), Not(c1), Not(c2), Not(c3))
sss.add(Not(negations))
print(sss.check())
print(sss.model())

Obtengo “sat”, con el modelo “[c_0 = True, c_3 = False, c_1 = False, c_2 = False]”, que cumple con la fórmula (no sé por qué se asignan las variables en ese orden).

Pero ahora, añado “And(Not(c_1), Not(c_2), Not(c_3))” a la fórmula (no es necesario entender por qué). Luego obtengo el resultado “unsat”, lo cual no tiene sentido. El resultado debería ser “sat”, por ejemplo, con el modelo “[c_0 = True, c_1 = False, c_2 = True, c_3 = False]”.

Aquí está el código:

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())

¿Alguna ayuda? Probé esto usando “Exists(c_0, c_1…)” explícitamente, pero el resultado es el mismo.

¡COMETÍ UN ERROR!

Falta una negación en “new_Negations = And(negations, Not(added_negations))”. Correctamente: “new_Negations = And(Not(negations), Not(added_negations))”.

Corrigiendo esto, el resultado vuelve a ser “sat”, concretamente, con un modelo: “[c_0 = False, c_3 = False, c_1 = True, c_2 = False]”.