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 integrates a number of widely used state-of-the-art SAT solvers. All the provided solvers are the original low-level implementations installed along with PySAT. Note that the solvers' source code is not a part of the project's source tree and is downloaded and patched at every PySAT installation. Note that originally the solvers' source code was not distributed with PySAT, which resulted in sequence of download and patch operations for each solver during each installation of PySAT. This, however, causes serious issues in case of using a proxy. As a result and since version 0.1.6.dev1, PySAT includes the solvers' archive files in the distribution.

Currently, the following SAT solvers are supported (at this point, for Minisat-based solvers only core versions are integrated):

• CaDiCaL (rel-1.0.3)
• CaDiCaL (rel-1.5.3)
• CaDiCaL (rel-1.9.5)
• Glucose (3.0)
• Glucose (4.1)
• Glucose (4.2.1)
• Lingeling (bbc-9230380-160707)
• MapleLCMDistChronoBT (SAT competition 2018 version)
• MapleCM (SAT competition 2018 version)
• Maplesat (MapleCOMSPS_LRB)
• Mergesat (3.0)
• Minicard (1.2)
• Minisat (2.2 release)
• Minisat (GitHub version)

In order to make SAT-based prototyping easier, PySAT integrates a variety of cardinality encodings. All of them are implemented from scratch in C++. The list of cardinality encodings included is the following:

• pairwise¹
• bitwise²
• sequential counters³
• sorting networks⁴
• cardinality networks⁵
• ladder/regular⁶⁷
• totalizer⁸
• modulo totalizer⁹
• iterative totalizer¹⁰

Furthermore, PySAT supports a number of encodings of pseudo-Boolean constraints listed below. This is done by exploiting a third-party library PyPBLib developed by the Logic Optimization Group of the University of Lleida. (PyPBLib is a wrapper over the known PBLib library¹¹.)

• binary decision diagrams (BDD)¹²¹³
• sequential weight counters¹⁴
• sorting networks¹⁵
• adder networks¹⁶
• and binary merge¹⁷

Finally, PySAT now supports arbitrary Boolean formulas with on-the-fly clausification¹⁸ and provides (pre-)processing functionality¹⁹ by exposing an interface to CaDiCaL's (version 1.5.3) preprocessor as well as external user-defined engines following the IPASIR-UP interface²⁰.

Boolean variables in PySAT are represented as natural identifiers, e.g. numbers from ℕ_> 0. A literal in PySAT is assumed to be an integer, e.g. -1 represents a literal ¬x₁ while 5 represents a literal x₅. A clause is a list of literals, e.g. [-3, -2] is a clause (¬x₃ ∨ ¬x₂).

The following is a trivial example of PySAT usage:

>>> from pysat.solvers import Glucose3
>>>
>>> g = Glucose3()
>>> g.add_clause([-1, 2])
>>> g.add_clause([-2, 3])
>>> print(g.solve())
>>> print(g.get_model())
...
True
[-1, -2, -3]

Another example shows how to extract unsatisfiable cores from a SAT solver given an unsatisfiable set of clauses:

>>> from pysat.solvers import Minisat22
>>>
>>> with Minisat22(bootstrap_with=[[-1, 2], [-2, 3]]) as m:
...     print(m.solve(assumptions=[1, -3]))
...     print(m.get_core())
...
False
[-3, 1]

Finally, the following example gives an idea of how one can extract a proof (supported by Glucose3, Glucose4, and Lingeling only):

>>> from pysat.formula import CNF
>>> from pysat.solvers import Lingeling
>>>
>>> formula = CNF()
>>> formula.append([-1, 2])
>>> formula.append([1, -2])
>>> formula.append([-1, -2])
>>> formula.append([1, 2])
>>>
>>> with Lingeling(bootstrap_with=formula.clauses, with_proof=True) as l:
...     if l.solve() == False:
...         print(l.get_proof())
...
['2 0', '1 0', '0']

PySAT usage is detailed in the provided examples. For instance, one can find simple PySAT-based implementations of

• Fu&Malik algorithm for MaxSAT²¹
• RC2/OLLITI algorithm for MaxSAT²²²³
• CLD-like algorithm for MCS extraction and enumeration²⁴
• LBX-like algorithm for MCS extraction and enumeration²⁵
• Deletion-based MUS extraction²⁶

The examples are installed with PySAT as a subpackage and, thus, they can be accessed internally in Python:

>>> from pysat.formula import CNF
>>> from pysat.examples.lbx import LBX
>>>
>>> formula = CNF(from_file='input.cnf')
>>> mcsls = LBX(formula)
>>>
>>> for mcs in mcsls.enumerate():
...     print(mcs)

Alternatively, they can be used as standalone executables, e.g. like this:

$ lbx.py -e all -d -s g4 -v another-input.wcnf

There are several ways to install PySAT. At this point, either way assumes you are using a POSIX-compliant operating system with GNU make and patch installed and available from the command line. Installation also relies on a C/C++ compiler supporting C++11, e.g. GCC or Clang, as well as the six Python package. Finally, in order to compile "C extensions" included as modules, the installer requires the headers of Python and zlib. Both can be installed using the standard package repositories.

Note that although version 0.1.5.dev1 of PySAT brings Microsoft Windows support, the toolkit was not extensively tested on this system. If you find out that something is broken on Windows, please, let us know. Your input is important.

Also note that using Clang is preferred on MacOS as there may be an issue with GCC being unaware of the command-line option --stdlib=libc++. Clang is available on MacOS by default. To enforce the installer to use it, you need to set the environment variable CC to /usr/bin/clang. For that, do export CC=/usr/bin/clang if using Bash, or setenv CC /usr/bin/clang if using tsch. This is not needed on Linux!

Once all the prerequisites are installed, the simplest way to get and start using PySAT is to install the latest stable release of the toolkit from PyPI:

$ pip install python-sat[aiger,approxmc,cryptosat,pblib]

We encourage you to install the optional dependencies pblib, aiger, approxmc, and cryptosat as in the previous command. However, if it cannot be done (e.g. if their installation fails), you can install PySAT with the functionality of aiger, approxmc, cryptosat, and pblib disabled:

$ pip install python-sat

Once installed from PyPI, the toolkit at a later stage can be updated in the following way:

$ pip install -U python-sat

Alternatively, one can clone the repository and execute the following command in the local copy:

$ python setup.py install

This will install the toolkit into the system's Python path. If another destination directory is preferred, it can be set by

$ python setup.py install --prefix=<where-to-install>

Both options (i.e. via pip or setup.py) are supposed to download and compile all the supported SAT solvers as well as prepare the installation of PySAT.

If PySAT has been significant to a project that leads to an academic publication, please, acknowledge that fact by citing PySAT:

@inproceedings{imms-sat18,
  author    = {Alexey Ignatiev and
               Antonio Morgado and
               Joao Marques{-}Silva},
  title     = {{PySAT:} {A} {Python} Toolkit for Prototyping
               with {SAT} Oracles},
  booktitle = {SAT},
  pages     = {428--437},
  year      = {2018},
  url       = {https://doi.org/10.1007/978-3-319-94144-8_26},
  doi       = {10.1007/978-3-319-94144-8_26}
}

PySAT toolkit is a work in progress. Although it can already be helpful in many practical settings (and it was successfully applied by its authors for a number of times), it would be great if some of the following additional features were implemented:

• more SAT solvers to support (e.g. RISS, Intel (R) SAT Solver among many others)
• lower level access to some of the solvers' internal parameters (e.g. variable activities, etc.)

These will require a significant effort to be made. Therefore, we would like to encourage the SAT community to contribute and make PySAT a tool for an easy and comfortable day-to-day use. :)

PySAT is licensed under MIT.