2026-07-17T11:05:36Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26331 2026-07-16T10:50:12Z ddc:004 open_access

d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries Masina, Gabriele Civini, Emanuele Michelutti, Massimo Spallitta, Giuseppe Sebastiani, Roberto SMT Knowledge Compilation d-DNNF 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 feasibility and effectiveness of the approach. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Gabriele Masina and Emanuele Civini and Massimo Michelutti and Giuseppe Spallitta and Roberto Sebastiani 2026 Is Part Of LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2026.25 urn:nbn:de:0030-drops-263316 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.25 eng https://creativecommons.org/licenses/by/4.0/legalcode