# Dsat: A Native SAT Solver for Discrete Logic

arXiv: https://arxiv.org/abs/2605.09347 · HTML: https://mlsanity.com/paper/2605.09347/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 9 of its 61 references that are in the map.
- First posted on arXiv 10 May 2026.

## Builds on (most cited first, 9 of 9)

- [Abduction-Based Explanations for Machine Learning Models](https://mlsanity.com/paper/1811.10656/) (2018)
- [A Symbolic Approach to Explaining Bayesian Network Classifiers](https://mlsanity.com/paper/1805.03364/) (2018)
- [On the Computational Intelligibility of Boolean Classifiers](https://mlsanity.com/paper/2104.06172/) (2021)
- [On the Computation of Necessary and Sufficient Explanations](https://mlsanity.com/paper/2203.10451/) (2022)
- [Logic for Explainable AI](https://mlsanity.com/paper/2305.05172/) (2023)
- [On Symbolically Encoding the Behavior of Random Forests](https://mlsanity.com/paper/2007.01493/) (2020)
- [A New Class of Explanations for Classifiers with Non-Binary Features](https://mlsanity.com/paper/2304.14760/) (2023)
- [Circuit Representations of Random Forests with Applications to XAI](https://mlsanity.com/paper/2602.08362/) (2026)
- [Proceedings of the 2023 XCSP3 Competition](https://mlsanity.com/paper/2312.05877/) (2023)

## Abstract (arXiv)

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.