pythonsatpysat

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?


Solution

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