PySAT: SAT technology in PythonΒΆ

PySAT is a Python (2.7, 3.4+) toolkit, which aims at providing a simple and unified interface to a number of state-of-art Boolean satisfiability (SAT) solvers as well as to a variety of cardinality and pseudo-Boolean encodings. The purpose of PySAT is to enable researchers working on SAT and its applications and generalizations to easily prototype with SAT oracles in Python while exploiting incrementally the power of the original low-level implementations of modern SAT solvers.

PySAT can be helpful when solving problems in NP but also beyond NP. For instance, PySAT is handy when one needs to quickly implement a MaxSAT solver, an MUS/MCS extractor or enumerator, an abstraction-based QBF solver, or any other kind of tool solving an application problem with the (potentially multiple and/or incremental) use of a SAT oracle.

PySAT is licensed under MIT.

_images/medals.svg