Welcome to PySAT’s documentation!#
This site covers the usage and API documentation of the PySAT toolkit. For the basic information on what PySAT is, please, see the main project website.
The PySAT toolkit has five core modules:
solvers. The four of them
solvers) are Python
wrappers for the code originally implemented in the C/C++ languages while the
formula module is a pure Python module. Version 0.1.4.dev0 of
PySAT brings a new module called
pb, which is a wrapper for the basic
functionality of a third-party library PyPBLib developed by the Logic Optimization
Group of the University of Lleida.
A supplementary sixth module
examples presents a list of scripts,
which are supposed to demonstrate how the toolkit can be used for practical
problem solving. The module includes a formula generator, several MaxSAT
solvers including an award-winning RC2, a few (S)MUS extractors and
enumerators as well as MCS enumerators, among other scripts.
Finally, an additional seventh module
allies brought by version
0.1.8.dev3 is meant to provide access to a number of third-party tools
important for practical SAT-based problem solving.
Core PySAT modules#
- Cardinality encodings (
- Boolean formula manipulation (
- Pseudo-Boolean encodings (
- Formula processing (
- SAT solvers’ API (
- Fu&Malik MaxSAT algorithm (
- Hard formula generator (
- Minimum/minimal hitting set solver (
- LBX-like MCS enumerator (
- LSU algorithm for MaxSAT (
- CLD-like MCS enumerator (
- An iterative model enumerator (
- A deletion-based MUS extractor (
- OptUx optimal MUS enumerator (
- RC2 MaxSAT solver (
This module provides interface to a list of external tools useful in practical SAT-based problem solving. Although only ApproxMCv4 is currently present here, the list of tools will grow.