Skip to content

Latest commit

 

History

History
374 lines (287 loc) · 14.2 KB

README.rst

File metadata and controls

374 lines (287 loc) · 14.2 KB
Raw

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.

Features

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):

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 [8]
  • bitwise [8]
  • sequential counters [9]
  • sorting networks [4]
  • cardinality networks [2]
  • ladder/regular [1] [5]
  • totalizer [3]
  • modulo totalizer [7]
  • iterative totalizer [6]
[1]Carlos Ansótegui, Felip Manyà. Mapping Problems with Finite-Domain Variables to Problems with Boolean Variables. SAT (Selected Papers) 2004. pp. 1-15
[2]Roberto Asin, Robert Nieuwenhuis, Albert Oliveras, Enric Rodriguez-Carbonell. Cardinality Networks and Their Applications. SAT 2009. pp. 167-180
[3]Olivier Bailleux, Yacine Boufkhad. Efficient CNF Encoding of Boolean Cardinality Constraints. CP 2003. pp. 108-122
[4]Kenneth E. Batcher. Sorting Networks and Their Applications. AFIPS Spring Joint Computing Conference 1968. pp. 307-314
[5]Ian P. Gent, Peter Nightingale. A New Encoding of Alldifferent Into SAT. In International workshop on modelling and reformulating constraint satisfaction problems 2004. pp. 95-110
[6]Ruben Martins, Saurabh Joshi, Vasco M. Manquinho, Inês Lynce. Incremental Cardinality Constraints for MaxSAT. CP 2014. pp. 531-548
[7]Toru Ogawa, Yangyang Liu, Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita. Modulo Based CNF Encoding of Cardinality Constraints and Its Application to MaxSAT Solvers. ICTAI 2013. pp. 9-17
[8](1, 2) Steven David Prestwich. CNF Encodings. Handbook of Satisfiability. 2009. pp. 75-97
[9]Carsten Sinz. Towards an Optimal CNF Encoding of Boolean Cardinality Constraints. CP 2005. pp. 827-831

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 [10].)

  • binary decision diagrams (BDD) [11] [12]
  • sequential weight counters [13]
  • sorting networks [11]
  • adder networks [11]
  • and binary merge [14]
[10]Tobias Philipp, Peter Steinke. PBLib - A Library for Encoding Pseudo-Boolean Constraints into CNF. SAT 2015. pp. 9-16
[11](1, 2, 3) Niklas Eén, Niklas Sörensson. Translating Pseudo-Boolean Constraints into SAT. JSAT. vol. 2(1-4). 2006. pp. 1-26
[12]Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell. BDDs for Pseudo-Boolean Constraints - Revisited. SAT. 2011. pp. 61-75
[13]Steffen Hölldobler, Norbert Manthey, Peter Steinke. A Compact Encoding of Pseudo-Boolean Constraints into SAT. KI. 2012. pp. 107-118
[14]Norbert Manthey, Tobias Philipp, Peter Steinke. A More Compact Translation of Pseudo-Boolean Constraints into CNF Such That Generalized Arc Consistency Is Maintained. KI. 2014. pp. 123-134

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

[21]G. S. Tseitin. On the complexity of derivations in the propositional calculus. Studies in Mathematics and Mathematical Logic, Part II. pp. 115–125, 1968
[22]Armin Biere, Matti Järvisalo, Benjamin Kiesl. Preprocessing in SAT Solving. In Handbook of Satisfiability - Second Edition. pp. 391-435
[23]Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere. IPASIR-UP: User Propagators for CDCL. SAT. 2023. pp. 8:1-8:13

Usage

Boolean variables in PySAT are represented as natural identifiers, e.g. numbers from \mathbb{N}_{>0}. A literal in PySAT is assumed to be an integer, e.g. -1 represents a literal \neg{x_1} while 5 represents a literal x_5. A clause is a list of literals, e.g. [-3, -2] is a clause (\neg{x_3} \vee \neg{x_2}).

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 [15]
  • RC2/OLLITI algorithm for MaxSAT [19] [20]
  • CLD-like algorithm for MCS extraction and enumeration [17]
  • LBX-like algorithm for MCS extraction and enumeration [18]
  • Deletion-based MUS extraction [16]
[15]Zhaohui Fu, Sharad Malik. On Solving the Partial MAX-SAT Problem. SAT 2006. pp. 252-265
[16]Joao Marques Silva. Minimal Unsatisfiability: Models, Algorithms and Applications. ISMVL 2010. pp. 9-14
[17]Joao Marques-Silva, Federico Heras, Mikolas Janota, Alessandro Previti, Anton Belov. On Computing Minimal Correction Subsets. IJCAI 2013. pp. 615-622
[18]Carlos Mencia, Alessandro Previti, Joao Marques-Silva. Literal-Based MCS Extraction. IJCAI 2015. pp. 1973-1979
[19]António Morgado, Carmine Dodaro, Joao Marques-Silva. Core-Guided MaxSAT with Soft Cardinality Constraints. CP 2014. pp. 564-573
[20]António Morgado, Alexey Ignatiev, Joao Marques-Silva. MSCG: Robust Core-Guided MaxSAT Solving. System Description. JSAT 2015. vol. 9, pp. 129-134

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

Installation

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

Note

For some shells, e.g. zsh, you may need to put the package names into single quotes, i.e. use pip install 'python-sat[aiger,approxmc,pblib]'.

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.

Citation

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}
}

To-Do

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. :)

License

PySAT is licensed under MIT.