pith. sign in

arxiv: 2603.09975 · v3 · pith:O5TTKPLVnew · submitted 2026-03-10 · 💻 cs.LO

d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries

Gabriele Masina , Emanuele Civini , Massimo Michelutti , Giuseppe Spallitta , Roberto Sebastiani This is my paper

Pith reviewed 2026-05-21 11:26 UTC · model grok-4.3

classification 💻 cs.LO
keywords knowledge compilationd-DNNFSMTtheory lemmaspolytime queriessatisfiability modulo theoriesmodel counting
0
0 comments X

The pith

SMT formulas combined with pre-computed theory lemmas can be compiled into d-DNNF for polytime queries using any standard propositional reasoner.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows how to lift knowledge compilation from propositional logic to satisfiability modulo theories. Before compiling an SMT formula into d-DNNF, a list of pre-computed theory lemmas is added so that theory-specific entailments are encoded at the propositional level. Once compiled, a wide range of SMT queries such as clausal entailment and model counting can be answered in polynomial time by an ordinary d-DNNF reasoner. The method works for every theory or theory combination and for every variant of d-DNNF, treating existing compilers and lemma generators as black boxes. A prototype implementation on top of current tools provides initial evidence that the approach is practical.

Core claim

By augmenting an input SMT formula with a sufficient list of pre-computed ad-hoc theory lemmas, the resulting propositional formula can be compiled into a d-DNNF whose queries correctly capture all SMT-level entailments and counting problems, allowing those queries to be solved in polynomial time by any standard propositional d-DNNF reasoner.

What carries the argument

The pre-compilation step that adds a list of theory lemmas to the SMT formula so that SMT queries reduce to propositional d-DNNF operations.

If this is right

  • After compilation, SMT clausal entailment and model counting are answered in polynomial time.
  • The same compiled structure supports every standard d-DNNF query at the SMT level.
  • The technique applies unchanged to any theory or combination of theories.
  • Existing d-DNNF compilers and theory-lemma enumerators can be used directly as black boxes.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The method could be applied to verification tasks that interleave Boolean and theory constraints, such as hybrid-system reachability.
  • Automatic selection of a minimal lemma set might keep compilation size small enough for larger formulas.
  • Similar lemma-augmentation ideas could be tested with other knowledge-compilation targets beyond d-DNNF.

Load-bearing premise

A sufficient collection of theory lemmas exists that can be added without producing an exponentially large d-DNNF or destroying the polynomial-time query guarantee.

What would settle it

An SMT formula for which every finite set of theory lemmas produces either an exponentially large d-DNNF or a d-DNNF that misses some SMT entailment or counting answer.

read the original abstract

In Knowledge Compilation (KC) a propositional knowledge base is compiled off-line into some target form, typically into deterministic decomposable negation normal form (d-DNNF) or one of its subcases, which is then used on-line to answer a large number of queries in polytime, such as clausal entailment, model counting, and others. The general idea is to push as much of the computational effort into the off-line compilation phase, which is amortized over all on-line polytime queries. In this paper, we present for the first time a novel and general technique to leverage d-DNNF compilation and querying to SMT level. Intuitively, before d-DNNF compilation, the input SMT formula is combined with a list of pre-computed ad-hoc theory lemmas, so that the queries at SMT level reduce to those at propositional level. This approach has several features: (i) it works for every theory, or theory combination thereof; (ii) it works for all forms of d-DNNF; (iii) it is easy to implement on top of any d-DNNF compiler and any theory-lemma enumerator, which are used as black boxes; (iv) most importantly, these compiled SMT d-DNNFs can be queried in polytime by means of a standard propositional d-DNNF reasoner. As proof of concept, we have implemented a tool on top of state-of-the-art d-DNNF packages and of the MathSAT SMT solver. Some preliminary empirical evaluation supports the effectiveness of the approach.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper presents a framework for extending knowledge compilation to SMT by augmenting an input SMT formula with a list of pre-computed ad-hoc theory lemmas before compiling it into d-DNNF. SMT-level queries (entailment, model counting, etc.) are then answered in polytime using a standard propositional d-DNNF reasoner. The approach is claimed to apply to arbitrary theories (or combinations), any d-DNNF variant, and to be realizable by treating existing d-DNNF compilers and theory-lemma enumerators as black boxes. A prototype implementation atop MathSAT and existing d-DNNF packages is described, together with preliminary empirical results.

Significance. If the reduction is semantics-preserving, the work would meaningfully bridge knowledge compilation and SMT, allowing amortization of expensive theory reasoning into an offline compilation phase while retaining polytime online queries. The black-box design and compatibility claims are practical strengths; the reported implementation and experiments provide concrete evidence of feasibility on selected benchmarks.

major comments (2)
  1. [§3] §3 (Framework and Reduction): The central claim that the augmented propositional formula yields correct SMT-level answers rests on the theory lemmas being complete for all relevant theory interactions. No formal completeness criterion is stated for the black-box enumerator relative to a given query set or propositional context; without it the reduction may omit lemmas that become necessary only after certain propositional assignments, undermining soundness of entailment and counting results.
  2. [§4] §4 (Query Equivalence Argument): The argument that standard d-DNNF operations on the compiled structure answer SMT queries correctly assumes that every unsatisfiable theory assignment is blocked by the added lemmas and that no spurious propositional entailments are introduced. The manuscript supplies no derivation or inductive argument establishing this equivalence for general T, which is load-bearing for the polytime SMT claim.
minor comments (2)
  1. [§2] The notation for theory atoms and lemma sets is introduced without a clear separation between propositional and theory-level variables in the running example; a small table contrasting the two would improve readability.
  2. [§6] The empirical section reports runtimes but does not tabulate the number or size of generated lemmas per instance; adding this would help assess whether the approach avoids the size-explosion concern raised in the framework.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive comments on our manuscript. The points raised concern the formal foundations of the proposed reduction, which we address below by committing to strengthen the presentation in the revised version.

read point-by-point responses

  1. Referee: [§3] §3 (Framework and Reduction): The central claim that the augmented propositional formula yields correct SMT-level answers rests on the theory lemmas being complete for all relevant theory interactions. No formal completeness criterion is stated for the black-box enumerator relative to a given query set or propositional context; without it the reduction may omit lemmas that become necessary only after certain propositional assignments, undermining soundness of entailment and counting results.

    Authors: We agree that an explicit completeness criterion is required for rigor. In the revision we will add a formal definition stating that the black-box enumerator must be complete relative to the input formula and query set: for every propositional assignment consistent with the formula, it must return every theory lemma entailed by the background theory under that assignment. This criterion directly prevents omission of context-dependent lemmas and thereby guarantees that the augmented propositional formula preserves SMT satisfiability, entailment, and model counts. revision: yes

  2. Referee: [§4] §4 (Query Equivalence Argument): The argument that standard d-DNNF operations on the compiled structure answer SMT queries correctly assumes that every unsatisfiable theory assignment is blocked by the added lemmas and that no spurious propositional entailments are introduced. The manuscript supplies no derivation or inductive argument establishing this equivalence for general T, which is load-bearing for the polytime SMT claim.

    Authors: We acknowledge that the current manuscript presents the equivalence at an intuitive level. The revision will contain a concise inductive argument on the d-DNNF structure. The base case shows that every theory-inconsistent assignment is blocked by at least one added lemma; the inductive step shows that the deterministic and decomposable properties are preserved under the augmentation, so that propositional entailment and counting on the compiled form coincide exactly with the corresponding SMT operations. This establishes the claimed polytime guarantees for arbitrary theories T. revision: yes

Circularity Check

0 steps flagged

No circularity: framework uses independent black-box components

full rationale

The paper describes a technique that augments an input SMT formula with a list of pre-computed ad-hoc theory lemmas prior to d-DNNF compilation, after which standard propositional d-DNNF queries are claimed to answer SMT-level questions in polynomial time. This construction treats both the d-DNNF compiler and the theory-lemma enumerator explicitly as external black boxes; no parameter is fitted to a subset of results and then re-used as a 'prediction,' no self-citation supplies a load-bearing uniqueness theorem, and no equation is defined in terms of its own output. The derivation therefore remains self-contained against external benchmarks and does not reduce to its own inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper builds on standard properties of d-DNNF and existing SMT solvers as black boxes; the main addition is the lemma-prepending integration step rather than new parameters or entities.

axioms (1)
  • standard math d-DNNF supports polytime queries for clausal entailment, model counting, and related tasks.
    Standard background result in knowledge compilation literature invoked to justify the final querying step.

pith-pipeline@v0.9.0 · 5825 in / 1364 out tokens · 68185 ms · 2026-05-21T11:26:25.065422+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

16 extracted references · 16 canonical work pages · 1 internal anchor

  1. [1]

    In: Handbook of Satisfiability, FAIA, vol

    doi:10.3233/FAIA201017. 2 Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Silvio Ranise, Peter van Rossum, and Roberto Sebastiani. Efficient Theory Combination via Boolean Search.Inf Comput, 204(10):1493–1525, 2006.doi:10.1016/j.ic.2005.05.011. 3 Randal E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation.IEEE Trans ...

    work page doi:10.3233/faia201017 2006

  2. [2]

    8 Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani

    doi:10.1007/ s00236-017-0297-2. 8 Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani. The Math- SAT5 SMT Solver. InTACAS 2013, LNCS, pages 93–107. Springer,

    work page 2013

  3. [3]

    9 Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani

    doi:10.1007/ 978-3-642-36742-7_7. 9 Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani. A Modular Approach to MaxSAT Modulo Theories. InSAT 2013, LNCS, pages 150–165. Springer,

    work page 2013

  4. [4]

    10 Alessandro Cimatti, Alberto Griggio, and Roberto Sebastiani

    doi: 10.1007/978-3-642-39071-5_12. 10 Alessandro Cimatti, Alberto Griggio, and Roberto Sebastiani. Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories.J Artif Intell Res, 40:701–728, 2011.doi:10.1613/jair.3196. 11 Emanuele Civini, Gabriele Masina, Giuseppe Spallitta, and Roberto Sebastiani. Beyond Eager Encodings: A Theory-Agnostic Appro...

    work page doi:10.1007/978-3-642-39071-5_12 2011

  5. [5]

    12 Adnan Darwiche

    arXiv:2602.14634,doi:10.48550/arXiv.2602.14634. 12 Adnan Darwiche. SDD: A New Canonical Representation of Propositional Knowledge Bases. InIJCAI 2011, volume 2 ofIJCAI’11, pages 819–826. AAAI Press,

    work page internal anchor Pith review doi:10.48550/arxiv.2602.14634 2011

  6. [6]

    J Artif Intell Res17(1), 229–264 (2002)

    doi:10.5591/ 978-1-57735-516-8/IJCAI11-143. 13 Adnan Darwiche and Pierre Marquis. A knowledge compilation map.J Artif Intell Res, 17(1):229–264, 2002.doi:10.1613/jair.989. 14 Vincent Derkinderen and Jean-Marie Lagniez. Circuit-Aware d-DNNF Compilation. InIJCAI 2025, volume 1, pages 4454–4462, 2025.doi:10.24963/ijcai.2025/496. 15 Vincent Derkinderen, Pedro...

    work page doi:10.1613/jair.989 2002

  7. [7]

    16 Pedro Zuidberg Dos Martires, Anton Dries, and Luc De Raedt

    URL:http://arxiv.org/abs/2306.04541,arXiv:2306.04541. 16 Pedro Zuidberg Dos Martires, Anton Dries, and Luc De Raedt. Exact and Approximate Weighted Model Integration with Probability Density Functions Using Knowledge Compilation. InAAAI 2019, volume 33, pages 7825–7833, 2019.doi:10.1609/aaai.v33i01.33017825. 17 Marco Gario and Andrea Micheli. PySMT: A sol...

    work page doi:10.1609/aaai.v33i01.33017825 2019

  8. [8]

    19 Jean-Marie Lagniez and Pierre Marquis

    doi:10.1023/A:1022988809947. 19 Jean-Marie Lagniez and Pierre Marquis. An Improved Decision-DNNF Compiler. InIJCAI 2017, pages 667–673. International Joint Conferences on Artificial Intelligence Organization,

    work page doi:10.1023/a:1022988809947 2017

  9. [9]

    20 d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries 20 Shuvendu K

    doi: 10.24963/ijcai.2017/93. 20 d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries 20 Shuvendu K. Lahiri, Robert Nieuwenhuis, and Albert Oliveras. SMT Techniques for Fast Predicate Abstraction. InCAV 2006, LNCS, pages 424–437. Springer, 2006.doi:10.1007/11817963_39. 21 Feifei Ma, Sheng Liu, and Jian Zhang. V olume Computation for Boolean...

    work page doi:10.24963/ijcai.2017/93 2017

  10. [10]

    22 Massimo Michelutti, Gabriele Masina, Giuseppe Spallitta, and Roberto Sebastiani

    doi:10.1007/ 978-3-642-02959-2_33. 22 Massimo Michelutti, Gabriele Masina, Giuseppe Spallitta, and Roberto Sebastiani. Canonical Decision Diagrams Modulo Theories. InECAI 2024, volume 392 ofFAIA, pages 4319–4327. IOS Press,

    work page 2024

  11. [11]

    In: (ECAI) 2024

    doi:10.3233/FAIA241007. 23 Jesper Møller, Jakob Lichtenberg, Henrik Reif Andersen, and Henrik Hulgaard. Difference Decision Diagrams. InCSL 1999, volume 1683 ofLNCS, pages 111–125. Springer,

    work page doi:10.3233/faia241007 1999

  12. [12]

    24 Paolo Morettin, Andrea Passerini, and Roberto Sebastiani

    doi:10.1007/ 3-540-48168-0_9. 24 Paolo Morettin, Andrea Passerini, and Roberto Sebastiani. Advanced SMT techniques for Weighted Model Integration.Artif Intell, 275(C):1–27, 2019.doi:10.1016/j.artint.2019.04.003. 25 Quoc-Sang Phan.Model Counting Modulo Theories. Thesis, Queen Mary University of London,

    work page doi:10.1016/j.artint.2019.04.003 2019

  13. [13]

    26 Roberto Sebastiani

    URL:https://qmro.qmul.ac.uk/xmlui/handle/123456789/15130. 26 Roberto Sebastiani. Colors Make Theories Hard. InIJCAR 2016, volume 9706 ofLNCS, pages 152–170. Springer, 2016.doi:10.1007/978-3-319-40229-1_11. 27 Arijit Shaw and Kuldeep S. Meel. Approximate SMT Counting Beyond Discrete Domains. InDAC, pages 1–7, 2025.doi:10.1109/DAC63849.2025.11133351. 28 Ari...

    work page doi:10.1007/978-3-319-40229-1_11 2016

  14. [14]

    In: FMCAD 2002

    URL: https://github.com/cuddorg/cudd. 30 Ofer Strichman. On Solving Presburger and Linear Arithmetic with SAT. InFMCAD 2002, pages 160–170. Springer, 2002.doi:10.1007/3-540-36126-X_10. 31 Ofer Strichman, Sanjit A. Seshia, and Randal E. Bryant. Deciding Separation Formulas with SAT. In CAV 2002, pages 209–222. Springer, 2002.doi:10.1007/3-540-45657-0_16. 3...

    work page doi:10.1007/3-540-36126-x_10 2002

  15. [15]

    33 Grigori S

    doi: 10.1145/3680465. 33 Grigori S. Tseitin. On the Complexity of Derivation in Propositional Calculus. InAutomation of Reasoning: 2: Classical Papers on Computational Logic 1967–1970, Symbolic Computation, pages 466–483. Springer, 1983.doi:10.1007/978-3-642-81955-1_28. 34 Jaco van de Pol and Olga Tveretina. A BDD-Representation for the Logic of Equality ...

    work page doi:10.1145/3680465 1967

  16. [16]

    proposition

    doi:10.1145/ 378239.378469. G. Masina, E. Civini, M. Michelutti, G. Spallitta, and R. Sebastiani 21 A Proofs In what follows “proposition” denote facts which are straighforward consequences of the definitions, whereas “lemma” and “theorem” denote facts for which we provide a proof explicitly. A.1 Some auxiliary propositions and lemmas ▶Proposition 28.Cons...

    work page arXiv