Recognition: no theorem link
Proof Systems Based on Structured Circuits
Pith reviewed 2026-05-13 02:30 UTC · model grok-4.3
The pith
SDDs and d-SDNNFs can refute some unsatisfiable CNFs with strictly smaller size than OBDDs.
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
We show that both SDD-based and d-SDNNF-based proof systems can provide strictly smaller refutations of unsatisfiable CNFs than their OBDD counterparts. We investigate the relative strength of these systems depending on which of the three fundamental derivation rules join, reordering, and weakening are allowed, obtaining several separations. To streamline the proofs we establish a sat-to-unsat lifting theorem that turns satisfiable CNFs hard to represent by SDDs and d-SDNNFs into unsatisfiable CNFs hard to refute in the corresponding proof systems.
What carries the argument
The sat-to-unsat lifting theorem, which converts satisfiable CNFs that are hard to represent by SDDs or d-SDNNFs into unsatisfiable CNFs that are hard to refute in the associated proof systems.
If this is right
- Some unsatisfiable CNFs admit strictly shorter refutations when lines are SDDs rather than OBDDs.
- The same holds when lines are d-SDNNFs rather than OBDDs.
- Allowing or forbidding join, reordering, and weakening produces incomparable proof systems in several cases.
- The lifting theorem preserves representation hardness when moving from satisfiable to unsatisfiable formulas.
Where Pith is reading between the lines
- The lifting construction may be reusable for other succinct representations in knowledge compilation.
- Implementation of these refutation systems could improve practical SAT solvers that already use circuit-based reasoning.
- The open problems on full rule-set comparisons point to a finer hierarchy of circuit-based proof complexity measures.
Load-bearing premise
The SDD and d-SDNNF formats together with the listed derivation rules form sound and complete proof systems whose size measures correspond to the claimed refutation lengths.
What would settle it
A concrete unsatisfiable CNF whose shortest refutation in the SDD or d-SDNNF system is larger than its shortest refutation in the OBDD system.
read the original 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.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper extends OBDD-based proof systems (introduced by Atserias, Kolaitis, and Vardi) to sentential decision diagrams (SDDs) and deterministic structured DNNF circuits (d-SDNNFs) for refuting unsatisfiable CNF formulas. It establishes that both new systems admit strictly smaller refutations than their OBDD counterparts. The relative strength of the systems is analyzed under subsets of the derivation rules join, reordering, and weakening, yielding separations and open problems. A sat-to-unsat lifting theorem is proven to convert representation-hard satisfiable CNFs into refutation-hard unsatisfiable CNFs.
Significance. If the constructions and proofs hold, the work advances the interface between knowledge compilation and proof complexity by showing that more succinct circuit representations can yield shorter proofs. The lifting theorem is a reusable tool for hardness transfers and the rule-based separations clarify the contribution of each inference rule. These results are of interest to both proof-complexity and SAT-solving communities.
major comments (2)
- [§4] §4 (or the section presenting the main separations): the claim that SDD and d-SDNNF systems give strictly smaller refutations than OBDD systems must be supported by explicit size bounds or families of formulas where the gap is super-constant; without a concrete lower-bound construction or reduction, the separation remains formal but not yet quantitatively verified.
- [§2–3] Definition of the proof systems (likely §2–3): completeness under the allowed rule subsets (join/reordering/weakening) is asserted but the argument that every unsatisfiable CNF has a finite refutation in each variant must be spelled out, especially when weakening is disallowed; otherwise the systems may not be proof systems in the standard sense.
minor comments (3)
- [Abstract / Introduction] The abstract and introduction use 'strictly smaller' without quantifying the gap; add a sentence clarifying whether the improvement is polynomial, exponential, or merely super-constant.
- [Preliminaries] Notation for d-SDNNF should be fixed early and used consistently; the distinction between deterministic and non-deterministic structured DNNFs is crucial for the size claims.
- [Lifting theorem section] The lifting theorem is presented as streamlining the proofs; a short self-contained statement of its precise hypothesis and conclusion would help readers apply it independently.
Simulated Author's Rebuttal
We thank the referee for the careful reading, positive evaluation, and constructive suggestions. We agree that both major comments identify areas where the presentation can be strengthened and will revise the manuscript accordingly.
read point-by-point responses
-
Referee: [§4] §4 (or the section presenting the main separations): the claim that SDD and d-SDNNF systems give strictly smaller refutations than OBDD systems must be supported by explicit size bounds or families of formulas where the gap is super-constant; without a concrete lower-bound construction or reduction, the separation remains formal but not yet quantitatively verified.
Authors: We thank the referee for this observation. The separations in the paper are obtained by applying the new sat-to-unsat lifting theorem to families of satisfiable CNFs that are already known (from the knowledge-compilation literature) to admit superpolynomial or exponential gaps between OBDD and SDD/d-SDNNF representations. While this yields strictly smaller refutations, the manuscript does not explicitly instantiate the lifting on a concrete family and compute the resulting numeric gaps. In the revised version we will add a short subsection (or appendix) that selects one standard separating family, states the known representation-size bounds, applies the lifting theorem, and derives explicit super-constant (in fact exponential) gaps between the OBDD-refutation size and the SDD/d-SDNNF-refutation size. revision: yes
-
Referee: [§2–3] Definition of the proof systems (likely §2–3): completeness under the allowed rule subsets (join/reordering/weakening) is asserted but the argument that every unsatisfiable CNF has a finite refutation in each variant must be spelled out, especially when weakening is disallowed; otherwise the systems may not be proof systems in the standard sense.
Authors: We agree that the completeness argument is only sketched and should be expanded. In the revised manuscript we will insert a self-contained lemma (or subsection) in §2–3 that proves completeness for every allowed subset of rules. The argument proceeds by showing that, using join and reordering alone, one can derive a structured circuit representation of the conjunction of all input clauses and then obtain a contradiction; when weakening is forbidden the same construction works because the rules suffice to simulate the necessary conjunctions and projections without needing to drop literals. We will also note that the presence of the empty clause as a target is sufficient for refutation completeness. revision: yes
Circularity Check
No significant circularity in derivation chain
full rationale
The paper introduces SDD- and d-SDNNF-based proof systems with subsets of the rules join/reordering/weakening, proves they yield strictly smaller refutations than OBDD counterparts on some unsatisfiable CNFs, and establishes a sat-to-unsat lifting theorem to transfer representation hardness to refutation hardness. No equations, definitions, or steps in the abstract or described contributions reduce any claimed separation or completeness result to a fitted parameter, self-referential definition, or unverified self-citation chain. The lifting theorem is explicitly presented as a new, independently interesting contribution rather than an input assumption, and the separations rest on explicit constructions. The derivation chain is therefore self-contained against external benchmarks.
Axiom & Free-Parameter Ledger
axioms (2)
- domain assumption Standard definitions and properties of OBDD, SDD, and d-SDNNF representations from knowledge compilation literature
- domain assumption The three derivation rules (join, reordering, weakening) are sound for the respective representations
Reference graph
Works this paper leans on
-
[1]
doi:10.1002/0471722154. 2 Albert Atserias, Phokion G. Kolaitis, and Moshe Y. Vardi. Constraint propagation as a proof system. In Mark Wallace, editor,Principles and Practice of Constraint Programming - CP 2004, 10th International Conference, CP 2004, Toronto, Canada, September 27 - October 1, 2004, Proceedings, volume 3258 ofLecture Notes in Computer Scie...
-
[2]
4 Simone Bova, Florent Capelli, Stefan Mengel, and Friedrich Slivovsky
URL:https://doi.org/10.1609/aaai.v30i1.10107,doi:10.1609/AAAI.V30I1.10107. 4 Simone Bova, Florent Capelli, Stefan Mengel, and Friedrich Slivovsky. A strongly exponential separation of dnnfs from cnf formulas,
-
[3]
5 Simone Bova, Florent Capelli, Stefan Mengel, and Friedrich Slivovsky
URL: https://arxiv.org/abs/1411.1995, arXiv:1411.1995. 5 Simone Bova, Florent Capelli, Stefan Mengel, and Friedrich Slivovsky. Knowledge compilation meets communication complexity. In Subbarao Kambhampati, editor,Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016, pages ...
-
[4]
6 Sam Buss, Dmitry Itsykson, Alexander Knop, Artur Riazanov, and Dmitry Sokolov
URL:http: //www.ijcai.org/Abstract/16/147. 6 Sam Buss, Dmitry Itsykson, Alexander Knop, Artur Riazanov, and Dmitry Sokolov. Lower bounds on OBDD proofs with several orders.ACM Trans. Comput. Log., 22(4):26:1–26:30, 2021.doi:10.1145/3468855. 7 Sam Buss, Dmitry Itsykson, Alexander Knop, and Dmitry Sokolov. Reordering rule makes OBDD proof systems stronger. ...
-
[5]
URL:https: //doi.org/10.4230/LIPIcs.CCC.2018.16,doi:10.4230/LIPICS.CCC.2018.16. 8 Adnan Darwiche. SDD: A new canonical representation of propositional knowledge bases. In Toby Walsh, editor,IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, Barcelona, Catalonia, Spain, July 16-22, 2011, pages 819–826. IJCAI/AAAI...
-
[6]
10 Alexis de Colnet and Stefan Mengel
URL:http://arxiv.org/abs/1106.1819,arXiv:1106.1819. 10 Alexis de Colnet and Stefan Mengel. Lower bounds on intermediate results in bottom-up knowledge compilation. InThirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, Thirty-Fourth Conference on Innovative Applications of Artificial Intelligence, IAAI 2022, The Twelveth Symposium on Educat...
-
[7]
11 Dmitry Itsykson, Alexander Knop, Andrei E
URL: https://doi.org/10.1609/aaai.v36i5.20496,doi:10.1609/AAAI.V36I5.20496. 11 Dmitry Itsykson, Alexander Knop, Andrei E. Romashchenko, and Dmitry Sokolov. On obdd-based algorithms and proof systems that dynamically change the order of variables. J. Symb. Log., 85(2):632–670,
-
[8]
12 Dmitry Itsykson and Artur Riazanov
URL:https://doi.org/10.1017/jsl.2019.53, doi: 10.1017/JSL.2019.53. 12 Dmitry Itsykson and Artur Riazanov. Automating OBDD proofs is np-hard. In Stefan Szeider, Robert Ganian, and Alexandra Silva, editors,47th International Symposium on Mathematical Foundations of Computer Science, MFCS 2022, August 22-26, 2022, Vienna, Austria, volume 241 ofLIPIcs, pages ...
-
[9]
13 Dmitry Itsykson, Artur Riazanov, and Petr Smirnov
URL: https://doi.org/10.4230/LIPIcs.MFCS.2022.59,doi:10.4230/LIPICS.MFCS.2022.59. 13 Dmitry Itsykson, Artur Riazanov, and Petr Smirnov. Tight bounds for tseitin formulas. In Kuldeep S. Meel and Ofer Strichman, editors,25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel, volume 236 X...
-
[10]
URL: https://doi.org/10.4230/LIPIcs.SAT.2022.6,doi:10.4230/LIPICS.SAT.2022.6. 14 Jan Krajícek. An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams.Electron. Colloquium Comput. Complex., TR07,
-
[11]
URL: https://eccc.weizmann.ac.il/eccc-reports/2007/TR07-007/index. html,arXiv:TR07-007. 15 Eyal Kushilevitz and Noam Nisan.Variable Partition Models, page 97–104. Cambridge University Press,
work page 2007
-
[12]
New compilation languages based on structured decomposability
16 Knot Pipatsrisawat and Adnan Darwiche. New compilation languages based on structured decomposability. In Dieter Fox and Carla P. Gomes, editors,Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence, AAAI 2008, Chicago, Illinois, USA, July 13-17, 2008, pages 517–522. AAAI Press,
work page 2008
-
[13]
URL:http://www.aaai.org/Library/AAAI/2008/ aaai08-082.php. 17 Igor Razgon. No small nondeterministic read-once branching programs for cnfs of bounded treewidth. In Marek Cygan and Pinar Heggernes, editors,Parameterized and Exact Computa- tion - 9th International Symposium, IPEC 2014, Wroclaw, Poland, September 10-12,
work page 2008
-
[14]
Springer, 2014.doi:10.1007/978-3-319-13524-3\_27
Revised Selected Papers, volume 8894 ofLecture Notes in Computer Science, pages 319–331. Springer, 2014.doi:10.1007/978-3-319-13524-3\_27. 18 Igor Razgon. On obdds for cnfs of bounded treewidth. InPrinciples of Knowledge Representa- tion and Reasoning: Proceedings of the Fourteenth International Conference, KR 2014, Vienna, Austria, July 20-24,
-
[15]
URL:http://www.aaai.org/ocs/index.php/ KR/KR14/paper/view/7982. 19 Nathan Segerlind. On the relative efficiency of resolution-like proofs and ordered binary decision diagram proofs. InProceedings of the 23rd Annual IEEE Conference on Computational Complexity, CCC 2008, 23-26 June 2008, College Park, Maryland, USA, pages 100–111. IEEE Computer Society, 200...
-
[16]
doi: 10.1145/7531.8928. 21 Harry Vinall-Smeeth. Structured d-dnnf is not closed under negation. InProceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI 2024, Jeju, South Korea, August 3-9, 2024, pages 3593–3601. ijcai.org,
-
[17]
22 Ingo Wegener.Branching Programs and Binary Decision Diagrams
URL:https://www.ijcai.org/ proceedings/2024/398. 22 Ingo Wegener.Branching Programs and Binary Decision Diagrams. SIAM,
work page 2024
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.