Document Open Access Logo

Towards Universally Accessible SAT Technology

Authors Alexey Ignatiev, Zi Li Tan, Christos Karamanos

PDF
Thumbnail PDF

File

LIPIcs.SAT.2024.16.pdf
  • Filesize: 0.93 MB
  • 11 pages

Document Identifiers

Author Details

Alexey Ignatiev
  • Monash University, Melbourne, Australia
Zi Li Tan
  • Monash University, Melbourne, Australia
Christos Karamanos
  • Monash University, Melbourne, Australia

Cite AsGet BibTex

Alexey Ignatiev, Zi Li Tan, and Christos Karamanos. Towards Universally Accessible SAT Technology. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 16:1-16:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.SAT.2024.16

Abstract

Boolean satisfiability (SAT) solvers are a family of highly efficient reasoning engines, which are frequently used for solving a large and diverse variety of practical challenges. This applies to multidisciplinary problems belonging to the class NP but also those arising at higher levels of the polynomial hierarchy. Unfortunately, encoding a problem of user’s interest to a (series of) propositional formula(s) in conjunctive normal form (CNF), let alone dealing with a SAT solver, is rarely a simple task even for an experienced SAT practitioner. This situation gets aggravated further when the user has little to no knowledge on the operation of the modern SAT solving technology. In 2018, the PySAT framework was proposed to address the issue of fast and "painless" prototyping with SAT solvers in Python allowing researchers to get SAT-based solutions to their problems without investing substantial time in the development process and yet sacrificing only a little in terms of performance. Since then, PySAT has proved a useful instrument for solving a wide range of practical problems and is now a critical package for the PyPI infrastructure. In the meantime, there have been advances in SAT solving and enhancements to PySAT functionality to extend its modelling and solving capabilities in order to make modern SAT technology accessible and deployable on a massive scale. This paper provides a high-level overview of the current architecture of PySAT and some of its capabilities including arbitrary Boolean formula manipulation, CNF preprocessing, and support for external user-defined propagators.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software libraries and repositories
  • Hardware → Theorem proving and SAT solving
  • Theory of computation → Constraint and logic programming
Keywords
  • PySAT
  • Python
  • Prototyping
  • Practical Applicability

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Josep Alos, Carlos Ansótegui, Josep M. Salvia, and Eduard Torres. OptiLog V2: model, solve, tune and run. In SAT, pages 25:1-25:16, 2022. Google Scholar
  2. Carlos Ansótegui, Jesus Ojeda, António Pacheco, Josep Pon, Josep M. Salvia, and Eduard Torres. OptiLog: A framework for SAT-based systems. In SAT, pages 1-10, 2021. Google Scholar
  3. Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonell. Cardinality networks and their applications. In SAT, pages 167-180, 2009. Google Scholar
  4. Gilles Audemard, Jean-Marie Lagniez, and Laurent Simon. Improving Glucose for incremental SAT solving with assumptions: Application to MUS extraction. In SAT, pages 309-317, 2013. Google Scholar
  5. Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern SAT solvers. In IJCAI, pages 399-404, 2009. Google Scholar
  6. Tomás Balyo, Armin Biere, Markus Iser, and Carsten Sinz. SAT race 2015. Artif. Intell., 241:45-65, 2016. Google Scholar
  7. Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability modulo theories. In Handbook of Satisfiability, pages 1267-1329. IOS Press, 2021. Google Scholar
  8. Clark W. Barrett and Cesare Tinelli. Satisfiability modulo theories. In Handbook of Model Checking, pages 305-343. Springer, 2018. Google Scholar
  9. Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions, volume B-2020-1, pages 51-53, 2020. Google Scholar
  10. Armin Biere, Matti Järvisalo, and Benjamin Kiesl. Preprocessing in SAT solving. In Handbook of Satisfiability, pages 391-435. IOS Press, 2021. Google Scholar
  11. Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia, and Moshe Y. Vardi. On parallel scalable uniform SAT witness generation. In TACAS, pages 304-319, 2015. Google Scholar
  12. Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi. Balancing scalability and uniformity in SAT witness generator. In DAC, pages 60:1-60:6, 2014. Google Scholar
  13. Karthekeyan Chandrasekaran, Richard M. Karp, Erick Moreno-Centeno, and Santosh S. Vempala. Algorithms for implicit hitting set problems. In SODA, pages 614-629, 2011. Google Scholar
  14. Tianqi Chen and Carlos Guestrin. XGBoost: A scalable tree boosting system. In KDD, pages 785-794, 2016. Google Scholar
  15. CryptoMiniSat. URL: https://github.com/msoos/cryptominisat/.
  16. Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver. In TACAS, pages 337-340, 2008. Google Scholar
  17. Niklas Eén and Armin Biere. Effective preprocessing in SAT through variable and clause elimination. In SAT, pages 61-75, 2005. Google Scholar
  18. Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In SAT, pages 502-518, 2003. Google Scholar
  19. Niklas Eén and Niklas Sörensson. Temporal induction by incremental SAT solving. Electronic Notes in Theoretical Computer Science, 89(4):543-560, 2003. Google Scholar
  20. Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, and Armin Biere. IPASIR-UP: user propagators for CDCL. In SAT, pages 8:1-8:13, 2023. Google Scholar
  21. Marco Gario and Andrea Micheli. PySMT: a solver-agnostic library for fast prototyping of SMT-based algorithms. In SMT Workshop, 2015. Google Scholar
  22. Glucose 3, Glucose 4.1, and Glucose 4.2.1. URL: http://www.labri.fr/perso/lsimon/glucose/.
  23. Alexey Ignatiev, Yacine Izza, Peter J. Stuckey, and João Marques-Silva. Using MaxSAT for efficient explanations of tree ensembles. In AAAI, pages 3776-3785, 2022. Google Scholar
  24. Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva. PySAT: A Python toolkit for prototyping with SAT oracles. In SAT, pages 428-437, 2018. Google Scholar
  25. Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva. RC2: an efficient MaxSAT solver. J. Satisf. Boolean Model. Comput., 11(1):53-64, 2019. Google Scholar
  26. Alexey Ignatiev, Nina Narodytska, and Joao Marques-Silva. Abduction-based explanations for machine learning models. In AAAI, pages 1511-1519, 2019. URL: https://doi.org/10.1609/AAAI.V33I01.33011511.
  27. Alexey Ignatiev, Alessandro Previti, Mark H. Liffiton, and Joao Marques-Silva. Smallest MUS extraction with minimal hitting set dualization. In CP, pages 173-182, 2015. Google Scholar
  28. Jia Hui Liang, Vijay Ganesh, Pascal Poupart, and Krzysztof Czarnecki. Learning rate based branching heuristic for SAT solvers. In SAT, pages 123-140, 2016. Google Scholar
  29. Mao Luo, Chu-Min Li, Fan Xiao, Felip Manyà, and Zhipeng Lü. An effective learnt clause minimization approach for CDCL SAT solvers. In IJCAI, pages 703-711, 2017. Google Scholar
  30. Norbert Manthey. The MergeSat solver. In SAT, pages 387-398, 2021. Google Scholar
  31. MapleSAT. URL: https://maplesat.github.io/.
  32. Joao Marques-Silva. Search algorithms for satisfiability problems in combinational switching circuits. PhD thesis, University of Michigan, 1995. Google Scholar
  33. João Marques-Silva and Alexey Ignatiev. Delivering trustworthy AI through formal XAI. In AAAI, pages 12342-12350, 2022. Google Scholar
  34. Joao Marques-Silva, Inês Lynce, and Sharad Malik. Conflict-driven clause learning SAT solvers. In Handbook of Satisfiability, pages 133-182. IOS Press, 2021. Google Scholar
  35. Joao Marques-Silva and Karem A. Sakallah. GRASP - a new search algorithm for satisfiability. In ICCAD, pages 220-227, 1996. Google Scholar
  36. Joao Marques-Silva and Karem A. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Computers, 48(5):506-521, 1999. Google Scholar
  37. MergeSat. URL: https://github.com/conp-solutions/mergesat.
  38. MiniCard 1.2. URL: https://github.com/liffiton/minicard/.
  39. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In DAC, pages 530-535, 2001. Google Scholar
  40. Alexander Nadel and Vadim Ryvchin. Chronological backtracking. In SAT, pages 111-121, 2018. Google Scholar
  41. Tobias Philipp and Peter Steinke. PBLib - A library for encoding pseudo-Boolean constraints into CNF. In SAT, pages 9-16, 2015. Google Scholar
  42. Knot Pipatsrisawat and Adnan Darwiche. A lightweight component caching scheme for satisfiability solvers. In SAT, pages 294-299, 2007. Google Scholar
  43. pycosat. URL: https://github.com/conda/pycosat.
  44. pylgl. URL: https://github.com/abfeldman/pylgl/.
  45. PyMiniSolvers. URL: https://github.com/liffiton/PyMiniSolvers/.
  46. Pyodide. URL: https://pyodide.org/.
  47. PyPBLib. URL: https://pypi.org/project/pypblib/.
  48. PyPI. URL: https://pypi.python.org/.
  49. PyPI 2FA Security Key Giveaway. URL: https://pypi.org/security-key-giveaway/.
  50. Olivier Roussel and Vasco M. Manquinho. Pseudo-Boolean and cardinality constraints. In Handbook of Satisfiability, pages 1087-1129. IOS Press, 2021. Google Scholar
  51. satispy. URL: https://github.com/netom/satispy/.
  52. Andy Shih, Arthur Choi, and Adnan Darwiche. A symbolic approach to explaining Bayesian network classifiers. In IJCAI, pages 5103-5111, 2018. URL: https://doi.org/10.24963/IJCAI.2018/708.
  53. Mate Soos. Enhanced gaussian elimination in dpll-based SAT solvers. In POS@SAT, pages 2-14, 2010. Google Scholar
  54. Mate Soos, Stephan Gocht, and Kuldeep S. Meel. Tinted, detached, and lazy CNF-XOR solving and its applications to counting and sampling. In CAV, pages 463-484, 2020. Google Scholar
  55. Mate Soos and Kuldeep S. Meel. BIRD: engineering an efficient CNF-XOR SAT solver and its applications to approximate model counting. In AAAI, pages 1592-1599, 2019. Google Scholar
  56. Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending SAT solvers to cryptographic problems. In SAT, pages 244-257, 2009. Google Scholar
  57. G. S. Tseitin. On the complexity of derivations in the propositional calculus. Studies in Mathematics and Mathematical Logic, Part II:115-125, 1968. Google Scholar
  58. Lintao Zhang, Conor F. Madigan, Matthew W. Moskewicz, and Sharad Malik. Efficient conflict driven learning in boolean satisfiability solver. In ICCAD, pages 279-285, 2001. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact