CODEWITHSUNDEEP
pythonsatpysat
Julia P.
Julia P.

Reputation: 37

PySAT convert a logical formula into a CNF without using Tseitin transformation

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?

Upvotes: 0

Views: 252

Answers (1)

alias
alias

Reputation: 30418

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

Upvotes: 0

Related Questions