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.

References in zbMATH (referenced in 18 articles , 1 standard article )

Showing results 1 to 18 of 18.
Sorted by year (citations)

  1. Ansótegui, Carlos; Ojeda, Jesús; Pacheco, Antonio; Pon, Josep; Salvia, Josep M.; Torres, Eduard: OptiLog: a framework for SAT-based systems (2021)
  2. Boltenhagen, Mathilde; Chatain, Thomas; Carmona, Josep: Optimized SAT encoding of conformance checking artefacts (2021)
  3. Ignatiev, Alexey; Marques-Silva, Joao: SAT-based rigorous explanations for decision lists (2021)
  4. Kochemazov, Stepan; Ignatiev, Alexey; Marques-Silva, Joao: Assessing progress in SAT solvers through the Lens of incremental SAT (2021)
  5. Kyrillidis, Anastasios; Shrivastava, Anshumali; Vardi, Moshe Y.; Zhang, Zhiwei: Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions (2021)
  6. 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)
  7. Peitl, Tomáš; Szeider, Stefan: Finding the hardest formulas for resolution (2021)
  8. Reichl, Franz-Xaver; Slivovsky, Friedrich; Szeider, Stefan: Certified DQBF solving by definition extraction (2021)
  9. Yu, Jinqiang; Ignatiev, Alexey; Stuckey, Peter J.; Le Bodic, Pierre: Learning optimal decision sets and lists with SAT (2021)
  10. Zhang, Yulin; Shell, Dylan A.: Cover combinatorial filters and their minimization problem (2021)
  11. Joseph Sweeney; Ruben Purdy; Ronald D Blanton; Lawrence Pileggi: CircuitGraph: A Python package for Boolean circuits (2020) not zbMATH
  12. Otpuschennikov, Ilya V.; Semenov, Alexander A.: Using merging variables-based local search to solve special variants of MaxSAT problem (2020)
  13. 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)
  14. Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao: RC2: an efficient MaxSAT solver (2019)
  15. Joshi, Saurabh; Kumar, Prateek; Rao, Sukrut; Martins, Ruben: \textsfOpen-WBO-Inc: approximation strategies for incomplete weighted MaxSAT (2019)
  16. Meuli, Giulia; Schmitt, Bruno; Ehlers, Rüdiger; Riener, Heinz; De Micheli, Giovanni: Evaluating ESOP optimization methods in quantum compilation flows (2019)
  17. Zha, Aolong; Koshimura, Miyuki; Fujita, Hiroshi: (N)-level modulo-based CNF encodings of pseudo-Boolean constraints for MaxSAT (2019)
  18. Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao: PySAT: a Python toolkit for prototyping with SAT oracles (2018)