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.
Currently, the following SAT solvers are supported (at this point, for Minisat-based solvers only core versions are integrated):
CaDiCaL (rel-1.0.3)
Glucose (3.0)
Glucose (4.1)
Lingeling (bbc-9230380-160707)
MapleLCMDistChronoBT (SAT competition 2018 version)
MapleCM (SAT competition 2018 version)
Maplesat (MapleCOMSPS_LRB)
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 8
bitwise 8
sequential counters 9
sorting networks 4
cardinality networks 2
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.)
- 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