The power of SAT technology in Python

Incremental SAT Solvers
PySAT aims at providing a simple and unified incremental interface to a number of state-of-art Boolean satisfiability (SAT) solvers.

Linear and Other Constraints
The toolkit provides a range of propositional encodings for linear (cardinality and pseudo-Boolean) constraints. It can also be paired with other packages to encode non-clausal constraints.

Performant Prototyping
PySAT is designed for simple, fast, and effective Python-based prototyping using SAT oracles.

Easy To Use
Widely used MiniSat-like incremental assumption-based interface of PySAT comes in handy when solving problems in NP but also beyond NP.

The toolkit is extensively documented. PySAT API description is additionally accompanied by a large number of examples provided, including MaxSAT solvers as well as MCS and MUS enumerators.

Open Source
Distributed under an MIT license, the PySAT toolkit is developed and maintained publicly on GitHub by SAT practitioners. You have a chance to improve PySAT. Pull requests are welcome!


Use the interactive shell to try PySAT in the browser

This is a WebAssembly power Python shell,
where you can try the examples in the browser:
1. Type code in the input cell and press
   Shift + Enter to execute;
2. Or copy paste the code, and click on
   the "Run" button in the toolbar
3. By the way, TAB-based autocompletion works!

# the standard way to import PySAT:
from pysat.formula import CNF
from pysat.solvers import Solver

# create a satisfiable CNF formula "(-x1 ∨ x2) ∧ (-x1 ∨ -x2)":
cnf = CNF(from_clauses=[[-1, 2], [-1, -2]])

# create a SAT solver for this formula:
with Solver(bootstrap_with=cnf) as solver:
    # 1.1 call the solver for this formula:
    print('formula is', f'{"s" if solver.solve() else "uns"}atisfiable')

    # 1.2 the formula is satisfiable and so has a model:
    print('and the model is:', solver.get_model())

    # 2.1 apply the MiniSat-like assumption interface:
    print('formula is',
        f'{"s" if solver.solve(assumptions=[1, 2]) else "uns"}atisfiable',
        'assuming x1 and x2')

    # 2.2 the formula is unsatisfiable,
    # i.e. an unsatisfiable core can be extracted:
    print('and the unsatisfiable core is:', solver.get_core())