Document Open Access Logo

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

Authors Gabriele Masina , Emanuele Civini , Massimo Michelutti , Giuseppe Spallitta , Roberto Sebastiani

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.25.pdf
  • Filesize: 6.11 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Theory of computation → Constraint and logic programming
  • Computing methodologies → Knowledge representation and reasoning
Keywords
  • SMT
  • Knowledge Compilation
  • d-DNNF

Metrics

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 feasibility and effectiveness of the approach.

Cite As Get BibTex

Gabriele Masina, Emanuele Civini, Massimo Michelutti, Giuseppe Spallitta, and Roberto Sebastiani. d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.25

Author Details

Gabriele Masina
  • DISI, University of Trento, Italy
Emanuele Civini
  • DISI, University of Trento, Italy
Massimo Michelutti
  • DISI, University of Trento, Italy
Giuseppe Spallitta
  • Rice University, Houston, TX, USA
Roberto Sebastiani
  • DISI, University of Trento, Italy

Funding

  • Sebastiani, Roberto: He was supported in part by the MUR PNRR project FAIR - Future AI Research (PE00000013) funded by the NextGenerationEU; he was partially funded under the NRRP, Mission 4 Component 2 Investment 1.4, by the European Union – NextGenerationEU (proj. nr. CN 00000013); he was supported in part by the TANGO project funded by the EU Horizon Europe research and innovation program under GA No 101120763. Views and opinions expressed are however those of the author only and do not necessarily reflect those of the European Union, the European Health and Digital Executive Agency (HaDEA) or The European Research Council. Neither the European Union nor the granting authority can be held responsible for them.

Supplementary Materials

References

  1. Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability Modulo Theories. In Handbook of Satisfiability, volume 336 of FAIA, pages 1267-1329. IOS Press, 2 edition, 2021. URL: https://doi.org/10.3233/FAIA201017.
  2. Randal E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans Comput, C-35(8):677-691, 1986. URL: https://doi.org/10.1109/TC.1986.1676819.
  3. Randal E. Bryant and Miroslav N. Velev. Boolean satisfiability with transitivity constraints. ACM Trans. Comput. Logic, 3(4):604-627, 2002. URL: https://doi.org/10.1145/566385.566390.
  4. Roberto Cavada, Alessandro Cimatti, Anders Franzén, Krishnamani Kalyanasundaram, Marco Roveri, and R.K. Shyamasundar. Computing Predicate Abstractions by Integrating BDDs and SMT Solvers. In FMCAD 2007, pages 69-76, 2007. URL: https://doi.org/10.1109/FAMCAD.2007.35.
  5. Sagar Chaki, Arie Gurfinkel, and Ofer Strichman. Decision diagrams for linear arithmetic. In FMCAD 2009, pages 53-60, 2009. URL: https://doi.org/10.1109/FMCAD.2009.5351143.
  6. Dmitry Chistikov, Rayna Dimitrova, and Rupak Majumdar. Approximate Counting in SMT and Value Estimation for Probabilistic Programs. Acta Inform., 54(8):729-764, 2017. URL: https://doi.org/10.1007/s00236-017-0297-2.
  7. Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani. The MathSAT5 SMT Solver. In TACAS 2013, LNCS, pages 93-107. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-36742-7_7.
  8. Emanuele Civini, Gabriele Masina, Giuseppe Spallitta, and Roberto Sebastiani. Beyond Eager Encodings: A Theory-Agnostic Approach to Theory-Lemma Enumeration in SMT. In IJCAR 2026, LNCS. Springer, 2026. Also arXiv preprint https://arxiv.org/abs/2602.14634. URL: https://doi.org/10.48550/arXiv.2602.14634.
  9. Adnan Darwiche. SDD: A New Canonical Representation of Propositional Knowledge Bases. In IJCAI 2011, volume 2 of IJCAI'11, pages 819-826. AAAI Press, 2011. URL: https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-143.
  10. Adnan Darwiche and Pierre Marquis. A knowledge compilation map. J Artif Intell Res, 17(1):229-264, 2002. URL: https://doi.org/10.1613/jair.989.
  11. Vincent Derkinderen and Jean-Marie Lagniez. Circuit-Aware d-DNNF Compilation. In IJCAI 2025, volume 1, pages 4454-4462, 2025. URL: https://doi.org/10.24963/ijcai.2025/496.
  12. Vincent Derkinderen, Pedro Zuidberg Dos Martires, Samuel Kolb, and Paolo Morettin. Top-Down Knowledge Compilation for Counting Modulo Theories, 2023. Workshop on Counting and Sampling at SAT 2023. URL: https://doi.org/10.48550/arXiv.2306.04541.
  13. Pedro Zuidberg Dos Martires, Anton Dries, and Luc De Raedt. Exact and Approximate Weighted Model Integration with Probability Density Functions Using Knowledge Compilation. In AAAI 2019, volume 33, pages 7825-7833, 2019. URL: https://doi.org/10.1609/aaai.v33i01.33017825.
  14. Marco Gario and Andrea Micheli. PySMT: A solver-agnostic library for fast prototyping of SMT-based algorithms. In SMT Workshop 2015, 2015. URL: https://github.com/pysmt/pysmt.
  15. Anuj Goel, Khurram Sajid, Hai Zhou, Adnan Aziz, and Vigyan Singhal. BDD Based Procedures for a Theory of Equality with Uninterpreted Functions. Form Methods Syst Des, 22(3):205-224, 2003. URL: https://doi.org/10.1023/A:1022988809947.
  16. Jean-Marie Lagniez and Pierre Marquis. An Improved Decision-DNNF Compiler. In IJCAI 2017, pages 667-673. International Joint Conferences on Artificial Intelligence Organization, 2017. URL: https://doi.org/10.24963/ijcai.2017/93.
  17. Shuvendu K. Lahiri, Robert Nieuwenhuis, and Albert Oliveras. SMT Techniques for Fast Predicate Abstraction. In CAV 2006, LNCS, pages 424-437. Springer, 2006. URL: https://doi.org/10.1007/11817963_39.
  18. Feifei Ma, Sheng Liu, and Jian Zhang. Volume Computation for Boolean Combination of Linear Arithmetic Constraints. In CADE 22, LNCS, pages 453-468. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02959-2_33.
  19. Gabriele Masina, Emanuele Civini, Massimo Michelutti, Giuseppe Spallitta, and Roberto Sebastiani. d-DNNF Modulo Theories - Experiments Source Code. Software, URL: https://github.com/ecivini/tddnnf-testbench (visited on 2026-05-26).
    Software Heritage Logo archived version
  20. Gabriele Masina, Emanuele Civini, Massimo Michelutti, Giuseppe Spallitta, and Roberto Sebastiani. d-DNNF Modulo Theories - Tool Source Code. Software, URL: https://github.com/ecivini/tddnnf (visited on 2026-05-26).
    Software Heritage Logo archived version
  21. Gabriele Masina, Emanuele Civini, Massimo Michelutti, Giuseppe Spallitta, and Roberto Sebastiani. d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries, 2026. (Extended version.). URL: https://doi.org/10.48550/arXiv.2603.09975.
  22. Massimo Michelutti, Gabriele Masina, Giuseppe Spallitta, and Roberto Sebastiani. Canonical Decision Diagrams Modulo Theories. In ECAI 2024, volume 392 of FAIA, pages 4319-4327. IOS Press, 2024. URL: https://doi.org/10.3233/FAIA241007.
  23. Jesper Møller, Jakob Lichtenberg, Henrik Reif Andersen, and Henrik Hulgaard. Difference Decision Diagrams. In CSL 1999, volume 1683 of LNCS, pages 111-125. Springer, 1999. URL: https://doi.org/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. URL: https://doi.org/10.1016/j.artint.2019.04.003.
  25. Quoc-Sang Phan. Model Counting Modulo Theories. Thesis, Queen Mary University of London, 2015. URL: https://qmro.qmul.ac.uk/xmlui/handle/123456789/15130.
  26. Roberto Sebastiani. Colors Make Theories Hard. In IJCAR 2016, volume 9706 of LNCS, pages 152-170. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-40229-1_11.
  27. Arijit Shaw and Kuldeep S. Meel. Approximate SMT Counting Beyond Discrete Domains. In DAC, pages 1-7, 2025. URL: https://doi.org/10.1109/DAC63849.2025.11133351.
  28. Arijit Shaw, Uddalok Sarkar, and Kuldeep S. Meel. Efficient Volume Computation for SMT Formulas. In KR 2025, volume 22, pages 544-554, 2025. URL: https://doi.org/10.24963/kr.2025/53.
  29. Fabio Somenzi. CUDD: CU decision diagram package. University of Colorado Boulder, 2009. URL: https://github.com/cuddorg/cudd.
  30. Ofer Strichman. On Solving Presburger and Linear Arithmetic with SAT. In FMCAD 2002, pages 160-170. Springer, 2002. URL: https://doi.org/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. URL: https://doi.org/10.1007/3-540-45657-0_16.
  32. Chico Sundermann, Heiko Raab, Tobias Heß, Thomas Thüm, and Ina Schaefer. Reusing d-DNNFs for Efficient Feature-Model Counting. ACM Trans. Softw. Eng. Methodol., 33(8):1-32, 2024. URL: https://doi.org/10.1145/3680465.
  33. Jaco van de Pol and Olga Tveretina. A BDD-Representation for the Logic of Equality and Uninterpreted Functions. In MFCS 2005, LNCS, pages 769-780. Springer, 2005. URL: https://doi.org/10.1007/11549345_66.
  34. Guy Van den Broeck, Nima Taghipour, Wannes Meert, Jesse Davis, and Luc De Raedt. Lifted Probabilistic Inference by First-Order Knowledge Compilation. In IJCAI 2011, IJCAI'11, pages 2178-2185. AAAI Press, 2011. URL: https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-363.
  35. Miroslav N. Velev and Randal E. Bryant. Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW. In DAC 2001, pages 226-231. ACM, 2001. URL: https://doi.org/10.1145/378239.378469.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact