PySAT: A Python toolkit for prototyping with SAT oracles. Boolean satisfiability (SAT) solvers are at the core of efficient approaches for solving a vast multitude of practical problems. Moreover, albeit targeting an NP-complete problem, SAT solvers are increasingly used for tackling problems beyond NP. Despite the success of SAT in practice, modeling with SAT and more importantly implementing SAT-based problem solving solutions is often a difficult and error-prone task. This paper proposes the PySAT toolkit, which enables fast Python-based prototyping using SAT oracles and SAT-related technology. PySAT provides a simple API for working with a few state-of-the-art SAT oracles and also integrates a number of cardinality constraint encodings, all aiming at simplifying the prototyping process. Experimental results presented in the paper show that PySAT-based implementations can be as efficient as those written in a low-level language.
Keywords for this software
References in zbMATH (referenced in 5 articles , 1 standard article )
Showing results 1 to 5 of 5.
- Joseph Sweeney; Ruben Purdy; Ronald D Blanton; Lawrence Pileggi: CircuitGraph: A Python package for Boolean circuits (2020) not zbMATH
- Semenov, Alexander; Otpuschennikov, Ilya; Gribanova, Irina; Zaikin, Oleg; Kochemazov, Stepan: Translation of algorithmic descriptions of discrete functions to SAT with applications to cryptanalysis problems (2020)
- Meuli, Giulia; Schmitt, Bruno; Ehlers, Rüdiger; Riener, Heinz; De Micheli, Giovanni: Evaluating ESOP optimization methods in quantum compilation flows (2019)
- Zha, Aolong; Koshimura, Miyuki; Fujita, Hiroshi: (N)-level modulo-based CNF encodings of pseudo-Boolean constraints for MaxSAT (2019)
- Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao: PySAT: A Python toolkit for prototyping with SAT oracles (2018)