DROPS

Document

DOI: 10.4230/LIPIcs.SAT.2026.31

Dsat: A Native SAT Solver for Discrete Logic

Authors: Yaofang Zhang, Ken Zhou, and Adnan Darwiche

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{zhang_et_al:LIPIcs.SAT.2026.31,
  author =	{Zhang, Yaofang and Zhou, Ken and Darwiche, Adnan},
  title =	{{Dsat: A Native SAT Solver for Discrete Logic}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{31:1--31:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.31},
  URN =		{urn:nbn:de:0030-drops-263372},
  doi =		{10.4230/LIPIcs.SAT.2026.31},
  annote =	{Keywords: Discrete Variables, CDCL SAT Solvers, Unit Resolution, Clause Learning}
}

Document

DOI: 10.4230/DagRep.7.9.62

Recent Trends in Knowledge Compilation (Dagstuhl Seminar 17381)

Authors: Adnan Darwiche, Pierre Marquis, Dan Suciu, and Stefan Szeider

Published in: Dagstuhl Reports, Volume 7, Issue 9 (2018)

Abstract

Knowledge compilation (KC) is a research topic which aims to investigate the possibility of circumventing the computational intractability of hard tasks, by preprocessing part of the available information, common to a number of instances. Pioneered almost three decades ago, KC is nowadays a very active research field, transversal to several areas within computer science. Among others, KC intersects knowledge representation, constraint satisfaction, algorithms, complexity theory, machine learning, and databases. The results obtained so far take various forms, from theory (compilability settings, definition of target languages for KC, complexity results, succinctness results, etc.) to more practical results (development and evaluation of compilers and other preprocessors, applications to diagnosis, planning, automatic configuration, etc.). Recently, KC has been positioned as providing a systematic method for solving problems beyond NP, and also found applications in machine learning. The goal of this Dagstuhl Seminar was to advance both aspects of KC, and to pave the way for a fruitful cross-fertilization between the topics, from theory to practice. The program included a mixture of long and short presentations, with discussions. Several long talks with a tutorial flavor introduced the participants to the variety of aspects in knowledge compilation and the diversity of techniques used. System presentations as well as an open problem session were also included in the program.

Cite as

Adnan Darwiche, Pierre Marquis, Dan Suciu, and Stefan Szeider. Recent Trends in Knowledge Compilation (Dagstuhl Seminar 17381). In Dagstuhl Reports, Volume 7, Issue 9, pp. 62-85, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{darwiche_et_al:DagRep.7.9.62,
  author =	{Darwiche, Adnan and Marquis, Pierre and Suciu, Dan and Szeider, Stefan},
  title =	{{Recent Trends in Knowledge Compilation (Dagstuhl Seminar 17381)}},
  pages =	{62--85},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2018},
  volume =	{7},
  number =	{9},
  editor =	{Darwiche, Adnan and Marquis, Pierre and Suciu, Dan and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.7.9.62},
  URN =		{urn:nbn:de:0030-drops-85896},
  doi =		{10.4230/DagRep.7.9.62},
  annote =	{Keywords: Knowledge compilation, Constraints, Preprocessing, Probabilistic databases, Model counting}
}

Search Results

Documents authored by Darwiche, Adnan

Dsat: A Native SAT Solver for Discrete Logic

Abstract

Cite as

Recent Trends in Knowledge Compilation (Dagstuhl Seminar 17381)

Abstract

Cite as

Thanks for your feedback!

Could not send message