d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries
2026-03-10 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors present a new way to apply a technique called d-DNNF compilation, which helps quickly answer logic questions, to a more complex area called SMT (Satisfiability Modulo Theories). Their method adds some extra helper statements to the SMT problem before compiling, making it possible to solve SMT queries using existing fast propositional logic tools. This works for any kind of theory and is easy to add to current systems. They built a tool combining these ideas and showed initial tests indicating it works well.
Knowledge Compilationd-DNNFSMTTheory LemmasModel CountingPropositional LogicPolytime QueriesMathSATDeterministic Decomposable Negation Normal Form
Authors
Gabriele Masina, Emanuale Civini, Massimo Michelutti, Giuseppe Spallitta, Roberto Sebastiani
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. 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.