PySAT
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 18 articles , 1 standard article )
Showing results 1 to 18 of 18.
Sorted by year (- Ansótegui, Carlos; Ojeda, Jesús; Pacheco, Antonio; Pon, Josep; Salvia, Josep M.; Torres, Eduard: OptiLog: a framework for SAT-based systems (2021)
- Boltenhagen, Mathilde; Chatain, Thomas; Carmona, Josep: Optimized SAT encoding of conformance checking artefacts (2021)
- Ignatiev, Alexey; Marques-Silva, Joao: SAT-based rigorous explanations for decision lists (2021)
- Kochemazov, Stepan; Ignatiev, Alexey; Marques-Silva, Joao: Assessing progress in SAT solvers through the Lens of incremental SAT (2021)
- Kyrillidis, Anastasios; Shrivastava, Anshumali; Vardi, Moshe Y.; Zhang, Zhiwei: Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions (2021)
- Mann, Makai; Wilson, Amalee; Zohar, Yoni; Stuntz, Lindsey; Irfan, Ahmed; Brown, Kristopher; Donovick, Caleb; Guman, Allison; Tinelli, Cesare; Barrett, Clark: Smt-Switch: a solver-agnostic C++ API for SMT solving (2021)
- Peitl, Tomáš; Szeider, Stefan: Finding the hardest formulas for resolution (2021)
- Reichl, Franz-Xaver; Slivovsky, Friedrich; Szeider, Stefan: Certified DQBF solving by definition extraction (2021)
- Yu, Jinqiang; Ignatiev, Alexey; Stuckey, Peter J.; Le Bodic, Pierre: Learning optimal decision sets and lists with SAT (2021)
- Zhang, Yulin; Shell, Dylan A.: Cover combinatorial filters and their minimization problem (2021)
- Joseph Sweeney; Ruben Purdy; Ronald D Blanton; Lawrence Pileggi: CircuitGraph: A Python package for Boolean circuits (2020) not zbMATH
- Otpuschennikov, Ilya V.; Semenov, Alexander A.: Using merging variables-based local search to solve special variants of MaxSAT problem (2020)
- 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)
- Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao: RC2: an efficient MaxSAT solver (2019)
- Joshi, Saurabh; Kumar, Prateek; Rao, Sukrut; Martins, Ruben: \textsfOpen-WBO-Inc: approximation strategies for incomplete weighted MaxSAT (2019)
- 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)