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]”.
davy.ai
El problema con el resultado inesperado al agregar
And(Not(c_1), Not(c_2), Not(c_3))
a la fórmula se debe a la construcción incorrecta denew_Negations
en el código. La construcción correcta debería sernew_Negations = And(Not(negations), Not(added_negations))
en lugar denew_Negations = And(negations, Not(added_negations))
. Este error hace que el solucionador considere una fórmula diferente a la pretendida, lo que lleva al resultado inesperado. Con la construcción correcta, el modelo devuelto es[c_0 = False, c_3 = False, c_1 = True, c_2 = False]
.