DROPS

Document

DOI: 10.4230/LIPIcs.SAT.2026.6

Proof Systems Based on Structured Circuits

Authors: Christoph Berkholz and Matthäus Micun

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

Abstract

Since their introduction by Atserias, Kolaitis, and Vardi in 2004, proof systems where each line is represented by an ordered binary decision diagram (OBDD) have been intensively studied as they allow to compactly represent Boolean functions. We extend this line of work by considering representation formats that can be even more succinct than OBDDs and have gained a lot of attention in the area of knowledge compilation: sentential decision diagrams (SDDs) and deterministic structured DNNF circuits (d-SDNNFs). We show that both variants can provide strictly smaller refutations of unsatisfiable CNFs than their OBDD counterparts. Furthermore, we investigate the relative strength of these systems depending on which of the three fundamental derivation rules join, reordering, and weakening are allowed. Here we obtain several separations and identify interesting open problems. To streamline our proofs we establish a sat-to-unsat lifting theorem that might be of independent interest: it turns satisfiable CNFs that are hard to represent by SDDs and d-SDNNFs into unsatisfiable CNFs that are hard to refute in the corresponding proof system.

Cite as

Christoph Berkholz and Matthäus Micun. Proof Systems Based on Structured Circuits. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{berkholz_et_al:LIPIcs.SAT.2026.6,
  author =	{Berkholz, Christoph and Micun, Matth\"{a}us},
  title =	{{Proof Systems Based on Structured Circuits}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{6:1--6:18},
  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.6},
  URN =		{urn:nbn:de:0030-drops-263123},
  doi =		{10.4230/LIPIcs.SAT.2026.6},
  annote =	{Keywords: Proof Complexity, Sentential Decision Diagram, DNNF, OBDD}
}

Search Results

Documents authored by Micun, Matthäus

Proof Systems Based on Structured Circuits

Abstract

Cite as

Thanks for your feedback!

Could not send message