Lesson 6

To conclude the section, let us get acquainted with the capabilities of another module \(\texttt{PySAT}\) in Python, which allows solving the satisfiability problem and provides more extensive functionality for this.

from pysat.solvers import Solver

clauses = [[2, -3], [-2], [3, 4], [-4, 1], [-1, -3]]

solver = Solver(bootstrap_with=clauses)
if solver.solve():
    print(solver.get_model())
else:
    print('Unsatisfiable')

[1, -2, -3, 4]