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.

Documented

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!

Try PySAT

```
"""
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())
```