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.
API documentation#
The PySAT toolkit has five core modules: card, formula,
pb, process and solvers. The four of them
(card, pb, process and 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#
Supplementary examples package#
- Fu&Malik MaxSAT algorithm (
pysat.examples.fm) - Hard formula generator (
pysat.examples.genhard) - Minimum/minimal hitting set solver (
pysat.examples.hitman) - LBX-like MCS enumerator (
pysat.examples.lbx) - LSU algorithm for MaxSAT (
pysat.examples.lsu) - CLD-like MCS enumerator (
pysat.examples.mcsls) - An iterative model enumerator (
pysat.examples.models) - A deletion-based MUS extractor (
pysat.examples.musx) - OptUx optimal MUS enumerator (
pysat.examples.optux) - RC2 MaxSAT solver (
pysat.examples.rc2)
Supplementary allies package#
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.