PySAT integrates a number of widely used stateoftheart SAT solvers. All the provided solvers are the original lowlevel 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 Minisatbased solvers only core versions are integrated):
 CaDiCaL (rel1.0.3)
 Glucose (3.0)
 Glucose (4.1)
 Lingeling (bbc9230380160707)
 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 SATbased 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^{1}
 bitwise^{1}
 sequential counters^{2}
 sorting networks^{3}
 cardinality networks^{4}
 ladder/regular^{5} ^{6}
 totalizer^{7}
 modulo totalizer^{8}
 iterative totalizer^{9}
Furthermore, PySAT supports a number of encodings of pseudoBoolean constraints listed below. This is done by exploiting a thirdparty 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}

Steven David Prestwich. CNF Encodings. Handbook of Satisfiability. 2009. pp. 7597 ↩︎ ↩︎

Carsten Sinz. Towards an Optimal CNF Encoding of Boolean Cardinality Constraints. CP 2005. pp. 827831 ↩︎

Kenneth E. Batcher. Sorting Networks and Their Applications. AFIPS Spring Joint Computing Conference 1968. pp. 307314 ↩︎

Roberto Asin, Robert Nieuwenhuis, Albert Oliveras, Enric RodriguezCarbonell. Cardinality Networks and Their Applications. SAT 2009. pp. 167180 ↩︎

Carlos Ansótegui, Felip Manyà. Mapping Problems with FiniteDomain Variables to Problems with Boolean Variables. SAT (Selected Papers) 2004. pp. 115 ↩︎

Ian P. Gent, Peter Nightingale. A New Encoding of Alldifferent Into SAT. In International workshop on modelling and reformulating constraint satisfaction problems 2004. pp. 95110 ↩︎

Olivier Bailleux, Yacine Boufkhad. Efficient CNF Encoding of Boolean Cardinality Constraints. CP 2003. pp. 108122 ↩︎

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

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

Tobias Philipp, Peter Steinke. PBLib  A Library for Encoding PseudoBoolean Constraints into CNF. SAT 2015. pp. 916 ↩︎

Niklas Eén, Niklas Sörensson. Translating PseudoBoolean Constraints into SAT. JSAT. vol. 2(14). 2006. pp. 126 ↩︎ ↩︎ ↩︎

Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric RodríguezCarbonell. BDDs for PseudoBoolean Constraints Revisited. SAT. 2011. pp. 6175 ↩︎

Steffen Hölldobler, Norbert Manthey, Peter Steinke. A Compact Encoding of PseudoBoolean Constraints into SAT. KI. 2012. pp. 107118 ↩︎

Norbert Manthey, Tobias Philipp, Peter Steinke. A More Compact Translation of PseudoBoolean Constraints into CNF Such That Generalized Arc Consistency Is Maintained. KI. 2014. pp. 123134 ↩︎