I have been using python’s library PySAT to create formulas, but I have been getting wrong results using this library’s solver. This is demo code to better explain the issue:
from pysat.solvers import Solver
from pysat.formula import *
a,b,c,d = Atom('a'), Atom('b'), Atom('c'), Atom('d')
formula = And(Or(a,b),c,d)
formula.clausify()
with Solver(name='g3') as solver:
solver.append_formula(formula.clauses)
if solver.solve():
print("SAT")
model = solver.get_model()
idp = Formula.export_vpool().id2obj
for k in model:
print('O' if k > 0 else 'X', abs(k), idp[abs(k)])
else:
print("UNSAT")
This code prints:
SAT
X 1 a
X 2 b
O 3 a | b
O 4 c
O 5 d
What is incorrect in this example: yes, while (a | b) is satisfiable, neither a or b are true.
In my program I am interested in atoms’ values, not recursive formulas.
Is there a way to avoid doing this manually?
You shouldn’t call clausify explicitly. The Formula class will handle that internally for you. So, code your problem as:
from pysat.solvers import Solver
from pysat.formula import *
a,b,c,d = Atom('a'), Atom('b'), Atom('c'), Atom('d')
formula = And(Or(a,b),c,d)
with Solver(name='g3') as solver:
solver.append_formula([c for c in formula])
if solver.solve():
print("SAT")
model = solver.get_model()
idp = Formula.export_vpool().id2obj
for k in model:
print('O' if k > 0 else 'X', abs(k), idp[abs(k)])
else:
print("UNSAT")
which prints:
SAT
O 1 a
X 2 b
O 3 a | b
O 4 c
O 5 d
(I’m not sure why you’re using 0 for 1 and X for -1 which is more traditional, but that’s besides the point.)