Document Open Access Logo

Dsat: A Native SAT Solver for Discrete Logic

Authors Yaofang Zhang , Ken Zhou , Adnan Darwiche

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.31.pdf
  • Filesize: 1.08 MB
  • 20 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Theory of computation → Logic and verification
Keywords
  • Discrete Variables
  • CDCL SAT Solvers
  • Unit Resolution
  • Clause Learning

Metrics

Abstract

Discrete variables are common in many applications, such as probabilistic reasoning, planning and explainable AI. When symbolic reasoning techniques are brought in to bear on these applications, a standard technique for handling discrete variables is to binarize them into Boolean variables to allow the use of Boolean computational machinery such as SAT solvers. This technique can face both computational and semantical challenges though. In this work, we develop a native SAT solver for discrete logic, which is a direct extension of Boolean logic in which variables can take arbitrary values. Our proposed solver has a similar design to Boolean SAT solvers, with ingredients such as unit resolution and clause learning but ones that operate natively on discrete variables. We illustrate the merits of the developed SAT solver by comparing it empirically to CSP solvers applied to discrete CNFs, to Boolean SAT solver applied to binarized CNFs, and to some hybrid solvers.

Cite As Get BibTex

Yaofang Zhang, Ken Zhou, and Adnan Darwiche. Dsat: A Native SAT Solver for Discrete Logic. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 31:1-31:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.31

Author Details

Yaofang Zhang
  • Department of Computer Science, University of California, Los Angeles, CA, USA
Ken Zhou
  • Department of Computer Science, University of California, Los Angeles, CA, USA
Adnan Darwiche
  • Department of Computer Science, University of California, Los Angeles, CA, USA

Acknowledgements

This work has been partially supported by ONR grant #N000142612296.

Supplementary Materials

References

  1. Carlos Ansótegui, Miquel Bofill, Felip Manyà, and Mateu Villaret. SAT and SMT technology for many-valued logics. Journal of Multiple-Valued Logic & Soft Computing, 2015. Google Scholar
  2. Carlos Ansótegui, Maria Luisa Bonet, Jordi Levy, and Felip Manyà. Mapping CSP into many-valued SAT. In João Marques-Silva and Karem A. Sakallah, editors, Theory and Applications of Satisfiability Testing - SAT 2007, 10th International Conference, Lisbon, Portugal, May 28-31, 2007, Proceedings, volume 4501 of Lecture Notes in Computer Science, pages 10-15. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-72788-0_4.
  3. Gilles Audemard, Steve Bellart, Louenas Bounia, Frédéric Koriche, Jean-Marie Lagniez, and Pierre Marquis. On the computational intelligibility of Boolean classifiers. In KR, pages 74-86, 2021. URL: https://doi.org/10.24963/KR.2021/8.
  4. Gilles Audemard, Frédéric Koriche, and Pierre Marquis. On tractable XAI queries based on compiled representations. In KR, pages 838-849, 2020. URL: https://doi.org/10.24963/KR.2020/86.
  5. Gilles Audemard, Christophe Lecoutre, and Emmanuel Lonca. Proceedings of the 2023 XCSP3 competition. CoRR, abs/2312.05877, 2023. URL: https://doi.org/10.48550/arXiv.2312.05877.
  6. Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern sat solvers. In IJCAI, volume 9, pages 399-404, 2009. URL: http://ijcai.org/Proceedings/09/Papers/074.pdf.
  7. Gilles Audemard and Laurent Simon. Refining restarts strategies for sat and unsat. In Michela Milano, editor, Principles and Practice of Constraint Programming, pages 118-126, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-33558-7_11.
  8. Gilles Audemard and Laurent Simon. On the glucose sat solver. International Journal on Artificial Intelligence Tools, 27(01):1840001, 2018. URL: https://doi.org/10.1142/S0218213018400018.
  9. Christer Bäckström and Bernhard Nebel. Complexity results for sas+ planning. Computational Intelligence, 11(4):625-655, 1995. URL: https://doi.org/10.1111/J.1467-8640.1995.TB00052.X.
  10. Tomáš Balyo, Armin Biere, Markus Iser, and Carsten Sinz. Sat race 2015. Artificial Intelligence, 241:45-65, 2016. URL: https://doi.org/10.1016/j.artint.2016.08.007.
  11. Bernhard Beckert, Reiner Hähnle, and Felip Manya. The SAT problem of signed CNF formulas. In Labelled Deduction, pages 59-80. Springer, 2000. Google Scholar
  12. Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. CaDiCaL 2.0. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I, volume 14681 of Lecture Notes in Computer Science, pages 133-152. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65627-9_7.
  13. Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. Cadical, gimsatul, isasat and kissat entering the sat competition 2024. Proc. of SAT Competition, 8, 2024. Google Scholar
  14. Armin Biere and Mathias Fleury. Gimsatul, IsaSAT and Kissat entering the SAT Competition 2022. In Tomas Balyo, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Competition 2022 - Solver and Benchmark Descriptions, volume B-2022-1 of Department of Computer Science Series of Publications B, pages 10-11. University of Helsinki, 2022. Google Scholar
  15. Mark Chavira and Adnan Darwiche. On probabilistic inference by weighted model counting. Artif. Intell., 172(6-7):772-799, 2008. URL: https://doi.org/10.1016/J.ARTINT.2007.11.002.
  16. Arthur Choi, Andy Shih, Anchal Goyanka, and Adnan Darwiche. On symbolically encoding the behavior of random forests. CoRR, abs/2007.01493, 2020. URL: https://arxiv.org/abs/2007.01493.
  17. Adnan Darwiche. A logical approach to factoring belief networks. In KR, pages 409-420. Morgan Kaufmann, 2002. Google Scholar
  18. Adnan Darwiche. Logic for explainable AI. In LICS, pages 1-11, 2023. URL: https://doi.org/10.1109/LICS56636.2023.10175757.
  19. Adnan Darwiche and Chunxi Ji. On the computation of necessary and sufficient explanations. In AAAI, pages 5582-5591. AAAI Press, 2022. URL: https://doi.org/10.1609/AAAI.V36I5.20498.
  20. Adnan Darwiche and Knot Pipatsrisawat. Complete algorithms. In Handbook of Satisfiability, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 101-132. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200986.
  21. Nachum Dershowitz, Ziyad Hanna, and Alexander Nadel. Towards a better understanding of the functionality of a conflict-driven sat solver. In João Marques-Silva and Karem A. Sakallah, editors, Theory and Applications of Satisfiability Testing - SAT 2007, pages 287-293, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-72788-0_27.
  22. Niklas Eén and Armin Biere. Effective preprocessing in sat through variable and clause elimination. In Fahiem Bacchus and Toby Walsh, editors, Theory and Applications of Satisfiability Testing, pages 61-75, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/11499107_5.
  23. Niklas Eén and Niklas Sörensson. An extensible sat-solver. In Enrico Giunchiglia and Armando Tacchella, editors, Theory and Applications of Satisfiability Testing, pages 502-518, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. Google Scholar
  24. Johannes K Fichte, Daniel Le Berre, Markus Hecher, and Stefan Szeider. The silent (r) evolution of sat. Communications of the ACM, 66(6):64-72, 2023. URL: https://doi.org/10.1145/3560469.
  25. Eibe Frank, Mark A Hall, and Ian H Witten. The weka workbench. online appendix for "Data mining: Practical machine learning tools and techniques", 2016. URL: https://hdl.handle.net/10289/17096.
  26. Robert M Haralick and Gordon L Elliott. Increasing tree search efficiency for constraint satisfaction problems. Artificial intelligence, 14(3):263-313, 1980. URL: https://doi.org/10.1016/0004-3702(80)90051-X.
  27. Malte Helmert. The fast downward planning system. Journal of Artificial Intelligence Research, 26:191-246, 2006. URL: https://doi.org/10.1613/JAIR.1705.
  28. Alexey Ignatiev, Nina Narodytska, Nicholas Asher, and João Marques-Silva. From contrastive to abductive explanations and back again. In AI*IA, volume 12414 of Lecture Notes in Computer Science, pages 335-355. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-77091-4_21.
  29. Alexey Ignatiev, Nina Narodytska, and João Marques-Silva. Abduction-based explanations for machine learning models. In Proceedings of the Thirty-Third Conference on Artificial Intelligence (AAAI), pages 1511-1519, 2019. URL: https://doi.org/10.1609/AAAI.V33I01.33011511.
  30. 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), pages 16-1. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.SAT.2024.16.
  31. Siddhartha Jain, Eoin O'Mahony, and Meinolf Sellmann. A complete multi-valued SAT solver. In David Cohen, editor, Principles and Practice of Constraint Programming - CP 2010 - 16th International Conference, CP 2010, St. Andrews, Scotland, UK, September 6-10, 2010. Proceedings, volume 6308 of Lecture Notes in Computer Science, pages 281-296. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15396-9_24.
  32. Chunxi Ji and Adnan Darwiche. A new class of explanations for classifiers with non-binary features. In JELIA, volume 14281 of Lecture Notes in Computer Science, pages 106-122. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-43619-2_8.
  33. Chunxi Ji and Adnan Darwiche. Circuit representations of random forests with applications to xai. In The 4th World Conference on Explainable Artificial Intelligence. Springer Nature Switzerland, 2026. URL: https://doi.org/10.48550/arXiv.2602.08362.
  34. Henry A. Kautz and Bart Selman. Planning as satisfiability. In Bernd Neumann, editor, 10th European Conference on Artificial Intelligence, ECAI 92, Vienna, Austria, August 3-7, 1992. Proceedings, pages 359-363. John Wiley and Sons, 1992. Google Scholar
  35. Mark H Liffiton and Jordyn C Maglalang. A cardinality solver: more expressive constraints for free. In International Conference on Theory and Applications of Satisfiability Testing, pages 485-486. Springer, 2012. Google Scholar
  36. Cong Liu, Andreas Kuehlmann, and Matthew W. Moskewicz. CAMA: A multi-valued satisfiability solver. In 2003 International Conference on Computer-Aided Design, ICCAD 2003, San Jose, CA, USA, November 9-13, 2003, pages 326-333. IEEE Computer Society / ACM, 2003. URL: https://doi.org/10.1109/ICCAD.2003.1257732.
  37. Mao Luo, Chu-Min Li, Fan Xiao, Felip Manyà, and Zhipeng Lü. An Effective Learnt Clause Minimization Approach for CDCL SAT Solvers. In Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI-17), pages 703-711, Melbourne, Australia, August 2017. URL: https://doi.org/10.24963/IJCAI.2017/98.
  38. J.P. Marques Silva and K.A. Sakallah. Grasp-a new search algorithm for satisfiability. In Proceedings of International Conference on Computer Aided Design, pages 220-227, 1996. URL: https://doi.org/10.1109/ICCAD.1996.569607.
  39. Matthew W Moskewicz, Conor F Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient sat solver. In Proceedings of the 38th annual Design Automation Conference, pages 530-535, 2001. URL: https://doi.org/10.1145/378239.379017.
  40. Alexander Nadel and Vadim Ryvchin. Chronological backtracking. In International Conference on Theory and Applications of Satisfiability Testing, pages 111-121. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_7.
  41. Nicholas Nethercote, Peter J Stuckey, Ralph Becket, Sebastian Brand, Gregory J Duck, and Guido Tack. Minizinc: Towards a standard cp modelling language. In International conference on principles and practice of constraint programming, pages 529-543. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74970-7_38.
  42. Laurent Perron, Frédéric Didier, and Steven Gay. The CP-SAT-LP solver (invited talk). In CP, volume 280 of LIPIcs, pages 3:1-3:2. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.CP.2023.3.
  43. Laurent Perron and Frédéric Didier. Cp-sat. URL: https://developers.google.com/optimization/cp/cp_solver/.
  44. Cédric Piette, Youssef Hamadi, and Lakhdar Sais. Vivifying propositional clausal formulae. In ECAI, volume 178, pages 525-529, 2008. URL: https://doi.org/10.3233/978-1-58603-891-5-525.
  45. Knot Pipatsrisawat and Adnan Darwiche. A lightweight component caching scheme for satisfiability solvers. In SAT, volume 4501 of Lecture Notes in Computer Science, pages 294-299. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-72788-0_28.
  46. Knot Pipatsrisawat and Adnan Darwiche. A new clause learning scheme for efficient unsatisfiability proofs. In AAAI, pages 1481-1484. AAAI Press, 2008. URL: http://www.aaai.org/Library/AAAI/2008/aaai08-243.php.
  47. Charles Prud’homme and Jean-Guillaume Fages. Choco-solver. Journal of Open Source Software, 7(78):4708, 2022. Google Scholar
  48. Jussi Rintanen. Planning and sat. In Handbook of Satisfiability: Second Edition, pages 765-789. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201003.
  49. Andy Shih, Arthur Choi, and Adnan Darwiche. A symbolic approach to explaining bayesian network classifiers. In IJCAI, pages 5103-5111. ijcai.org, 2018. URL: https://doi.org/10.24963/IJCAI.2018/708.
  50. Niklas Sörensson and Armin Biere. Minimizing learned clauses. In Oliver Kullmann, editor, Theory and Applications of Satisfiability Testing - SAT 2009, pages 237-243, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-02777-2_23.
  51. Peter J. Stuckey. Lazy clause generation: Combining the power of SAT and CP (and mip?) solving. In CPAIOR, volume 6140 of Lecture Notes in Computer Science, pages 5-9. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-13520-0_3.
  52. Peter J. Stuckey, Thibaut Feydy, Andreas Schutt, Guido Tack, and Julien Fischer. The minizinc challenge 2008-2013. AI Mag., 35(2):55-60, 2014. URL: https://doi.org/10.1609/AIMAG.V35I2.2539.
  53. Hantao Zhang and Mark Stickel. An efficient algorithm for unit propagation. In Proceedings of the Fourth International Symposium on Artificial Intelligence and Mathematics, 96, 1996. Google Scholar
  54. Lintao Zhang, Conor F. Madigan, Matthew W. Moskewicz, and Sharad Malik. Efficient conflict driven learning in boolean satisfiability solver. In ICCAD, pages 279-285. IEEE Computer Society, 2001. URL: https://doi.org/10.1109/ICCAD.2001.968634.
  55. Yaofang Zhang, Ken Zhou, and Adnan Darwiche. Dsat: A native sat solver for discrete logic, 2026. URL: https://arxiv.org/abs/2605.09347.
  56. Neng-Fa Zhou and Håkan Kjellerstrand. The Picat-SAT compiler. In PADL, volume 9585 of Lecture Notes in Computer Science, pages 48-62. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-28228-2_4.
  57. Neng-Fa Zhou and Håkan Kjellerstrand. Optimizing SAT encodings for arithmetic constraints. In CP, volume 10416 of Lecture Notes in Computer Science, pages 671-686. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66158-2_43.
  58. Neng-Fa Zhou, Håkan Kjellerstrand, and Jonathan Fruhman. Constraint Solving and Planning with Picat. Springer Briefs in Intelligent Systems. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-25883-6.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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