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:

  • pairwise1
  • bitwise1
  • sequential counters2
  • sorting networks3
  • cardinality networks4
  • ladder/regular5 6
  • totalizer7
  • modulo totalizer8
  • iterative totalizer9

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

  • binary decision diagrams (BDD)11 12
  • sequential weight counters13
  • sorting networks11
  • adder networks11
  • and binary merge14

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

  1. Steven David Prestwich. CNF Encodings. Handbook of Satisfiability. 2009. pp. 75-97 ↩︎ ↩︎

  2. Carsten Sinz. Towards an Optimal CNF Encoding of Boolean Cardinality Constraints. CP 2005. pp. 827-831 ↩︎

  3. Kenneth E. Batcher. Sorting Networks and Their Applications. AFIPS Spring Joint Computing Conference 1968. pp. 307-314 ↩︎

  4. Roberto Asin, Robert Nieuwenhuis, Albert Oliveras, Enric Rodriguez-Carbonell. Cardinality Networks and Their Applications. SAT 2009. pp. 167-180 ↩︎

  5. Carlos Ansótegui, Felip Manyà. Mapping Problems with Finite-Domain Variables to Problems with Boolean Variables. SAT (Selected Papers) 2004. pp. 1-15 ↩︎

  6. 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 ↩︎

  7. Olivier Bailleux, Yacine Boufkhad. Efficient CNF Encoding of Boolean Cardinality Constraints. CP 2003. pp. 108-122 ↩︎

  8. 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 ↩︎

  9. Ruben Martins, Saurabh Joshi, Vasco M. Manquinho, Inês Lynce. Incremental Cardinality Constraints for MaxSAT. CP 2014. pp. 531-548 ↩︎

  10. Tobias Philipp, Peter Steinke. PBLib - A Library for Encoding Pseudo-Boolean Constraints into CNF. SAT 2015. pp. 9-16 ↩︎

  11. 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 ↩︎

  15. G. S. Tseitin. On the complexity of derivations in the propositional calculus. Studies in Mathematics and Mathematical Logic, Part II. pp. 115–125, 1968 ↩︎

  16. Armin Biere, Matti Järvisalo, Benjamin Kiesl. Preprocessing in SAT Solving. In Handbook of Satisfiability - Second Edition. pp. 391-435 ↩︎

  17. 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 ↩︎