2026-07-20T06:34:01Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26337 2026-07-16T10:50:12Z ddc:004 open_access

Dsat: A Native SAT Solver for Discrete Logic Zhang, Yaofang Zhou, Ken Darwiche, Adnan Discrete Variables CDCL SAT Solvers Unit Resolution Clause Learning 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Yaofang Zhang and Ken Zhou and Adnan Darwiche 2026 Is Part Of LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2026.31 urn:nbn:de:0030-drops-263372 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.31 eng https://creativecommons.org/licenses/by/4.0/legalcode