Document Open Access Logo

decdnnf_rs: A Framework for Querying d-DNNF (Tool Paper)

Authors Jean-Marie Lagniez , Emmanuel Lonca

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.38.pdf
  • Filesize: 0.83 MB
  • 12 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Knowledge compilation
  • d-DNNF
  • Model counting
  • Model enumeration
  • Uniform sampling

Metrics

Abstract

Industrial automated reasoning demands the rapid, repeated extraction of insights from complex formulas. Knowledge compilation into the Deterministic Decomposable Negation Normal Form (d-DNNF) addresses this by reducing natively intractable tasks to polynomial-time operations. We present decdnnf_rs, a performant framework for executing advanced reasoning queries directly on d-DNNF circuits. The library provides unified support for Satisfiability, Model Counting, Disjoint Model Enumeration, Direct Access, and Uniform Sampling. Crucially, decdnnf_rs handles dynamic contexts through implicit conditioning via weight propagation, avoiding the computational overhead of explicit graph modification. It also incorporates dynamic smoothness tracking to maintain a compact memory footprint. Bridging theoretical advancements with robust software engineering, decdnnf_rs offers an optimized toolset for exact and stochastic reasoning.

Cite As Get BibTex

Jean-Marie Lagniez and Emmanuel Lonca. decdnnf_rs: A Framework for Querying d-DNNF (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 38:1-38:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.38

Author Details

Jean-Marie Lagniez
  • Univ. Artois, CNRS, CRIL, Lens, France
Emmanuel Lonca
  • Univ. Artois, CNRS, CRIL, Lens, France

Funding

This work has been partly supported by the CERADOC project of the French National Agency for Research (ANR-25-CE23-3078).

Supplementary Materials

References

  1. Jean-Marc Astesana, Laurent Cosserat, and Hélène Fargier. Constraint-based vehicle configuration: A case study. In 22nd IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2010, Arras, France, 27-29 October 2010 - Volume 1, pages 68-75. IEEE Computer Society, 2010. Google Scholar
  2. Teodora Baluta, Zheng Leong Chua, Kuldeep S. Meel, and Prateek Saxena. Scalable quantitative verification for deep neural networks. In 43rd IEEE/ACM International Conference on Software Engineering, ICSE 2021, Madrid, Spain, 22-30 May 2021, pages 312-323. IEEE, 2021. Google Scholar
  3. Armin Biere, Katalin Fazekas, Mathias Fleury, and Nils Froleyks. Clausal equivalence sweeping paper logs (version 1). https://doi.org/10.5281/zenodo.11203283, May 2024.
  4. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2021. Google Scholar
  5. Armin Biere, Jean-Marie Lagniez, and Emmanuel Lonca. Efficient minimization of Decision-DNNF circuits via semantic hashing and provenance tracking [to appear]. In Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-ECAI 2026, Bremen, Germany, August 15-21, 2026, 2026. Google Scholar
  6. 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 1008-1014. IJCAI/AAAI Press, 2016. Available from: URL: http://www.ijcai.org/Abstract/16/147.
  7. Ronald J. Brachman and Hector J. Levesque. Knowledge Representation and Reasoning. Elsevier, 2004. Available from: URL: http://www.elsevier.com/wps/find/bookdescription.cws_home/702602/description.
  8. Karl Bringmann, Nofar Carmeli, and Stefan Mengel. Tight fine-grained bounds for direct access on join queries. ACM Trans. Database Syst., 50(1):1:1-1:44, 2025. Google Scholar
  9. Randal E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers, 35(8):677-691, 1986. Google Scholar
  10. Marco Cadoli and Francesco M. Donini. A survey on knowledge compilation. AI Commun., 10(3-4):137-150, 1997. Available from: URL: http://content.iospress.com/articles/ai-communications/aic133.
  11. Nofar Carmeli, Nikolaos Tziavelis, Wolfgang Gatterbauer, Benny Kimelfeld, and Mirek Riedewald. Tractable orders for direct access to ranked answers of conjunctive queries. ACM Trans. Database Syst., 48(1):1:1-1:45, 2023. Google Scholar
  12. Stephen A. Cook. The complexity of theorem-proving procedures. In Michael A. Harrison, Ranan B. Banerji, and Jeffrey D. Ullman, editors, Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, May 3-5, 1971, Shaker Heights, Ohio, USA, pages 151-158. ACM, 1971. Google Scholar
  13. Adnan Darwiche. A compiler for deterministic, decomposable negation normal form. In Rina Dechter, Michael J. Kearns, and Richard S. Sutton, editors, Proceedings of the Eighteenth National Conference on Artificial Intelligence and Fourteenth Conference on Innovative Applications of Artificial Intelligence, July 28 - August 1, 2002, Edmonton, Alberta, Canada, pages 627-634. AAAI Press / The MIT Press, 2002. Available from: URL: http://www.aaai.org/Library/AAAI/2002/aaai02-094.php.
  14. Adnan Darwiche. New advances in compiling CNF into decomposable negation normal form. In Ramón López de Mántaras and Lorenza Saitta, editors, Proceedings of the 16th Eureopean Conference on Artificial Intelligence, ECAI'2004, including Prestigious Applicants of Intelligent Systems, PAIS 2004, Valencia, Spain, August 22-27, 2004, pages 328-332. IOS Press, 2004. Google Scholar
  15. Adnan Darwiche. Modeling and Reasoning with Bayesian Networks. Cambridge University Press, 2009. Available from: URL: http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=9780521884389.
  16. 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, 2011. Google Scholar
  17. Adnan Darwiche. Artificial intelligence framework developed by UCLA professor now powers Toyota websites. https://newsroom.ucla.edu/releases/artificial-intelligence-framework-developed-by-ucla-professor-now-powers-toyota-websites, 2014. Accessed: 2026-02-19.
  18. Adnan Darwiche. Logic for explainable AI. In 38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023, Boston, MA, USA, June 26-29, 2023, pages 1-11. IEEE, 2023. Google Scholar
  19. Adnan Darwiche and Pierre Marquis. A knowledge compilation map. J. Artif. Intell. Res., 17:229-264, 2002. Google Scholar
  20. Hélène Fargier and Pierre Marquis. On the use of partially ordered decision graphs in knowledge compilation and quantified boolean formulae. In Proceedings, The Twenty-First National Conference on Artificial Intelligence and the Eighteenth Innovative Applications of Artificial Intelligence Conference, July 16-20, 2006, Boston, Massachusetts, USA, pages 42-47. AAAI Press, 2006. Available from: URL: http://www.aaai.org/Library/AAAI/2006/aaai06-007.php.
  21. Rafael Kiesel and Thomas Eiter. Knowledge compilation and more with SharpSAT-TD. In Pierre Marquis, Tran Cao Son, and Gabriele Kern-Isberner, editors, Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning, KR 2023, Rhodes, Greece, September 2-8, 2023, pages 406-416, 2023. Google Scholar
  22. Andreas Kuehlmann. Dynamic transition relation simplification for bounded property checking. In 2004 International Conference on Computer-Aided Design, ICCAD 2004, San Jose, CA, USA, November 7-11, 2004, pages 50-57. IEEE Computer Society / ACM, 2004. Google Scholar
  23. Jean-Marie Lagniez and Emmanuel Lonca. Leveraging decision-DNNF compilation for enumerating disjoint partial models. In Pierre Marquis, Magdalena Ortiz, and Maurice Pagnucco, editors, Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning, KR 2024, Hanoi, Vietnam. November 2-8, 2024, 2024. Google Scholar
  24. Jean-Marie Lagniez and Emmanuel Lonca. Enhancing query efficiency for D-DNNF representations through preprocessing. In Giovanni Casini, Besik Dundua, and Temur Kutsia, editors, Logics in Artificial Intelligence - 19th European Conference, JELIA 2025, Kutaisi, Georgia, September 1-4, 2025, Proceedings, Part II, volume 16094 of Lecture Notes in Computer Science, pages 125-140. Springer, 2025. Google Scholar
  25. Jean-Marie Lagniez and Emmanuel Lonca. crillab/decdnnf_rs. https://github.com/crillab/decdnnf_rs, 2026. Accessed on March 13, 2026. . URL: https://github.com/crillab/decdnnf_rs
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.26963
  26. Jean-Marie Lagniez and Emmanuel Lonca. crillab/decdnnf_rs_c. https://github.com/crillab/decdnnf_rs_c, 2026. Accessed on March 13, 2026. . URL: https://github.com/crillab/decdnnf_rs_c
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.26964
  27. Jean-Marie Lagniez and Emmanuel Lonca. crillab/decdnnf_rs_py. https://github.com/crillab/decdnnf_rs_py, 2026. Accessed on March 13, 2026. . URL: https://github.com/crillab/decdnnf_rs_py
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.26965
  28. Jean-Marie Lagniez and Emmanuel Lonca. decdnnf_rs - crates.io: Rust package registry. https://crates.io/crates/decdnnf_rs, 2026. Accessed on March 13, 2026.
  29. Jean-Marie Lagniez and Pierre Marquis. An improved decision-DNNF compiler. In Carles Sierra, editor, Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, pages 667-673. ijcai.org, 2017. Google Scholar
  30. Feng Lu, Li-C. Wang, Kwang-Ting Cheng, and Ric C.-Y. Huang. A circuit SAT solver with signal correlation guided learning. In 2003 Design, Automation and Test in Europe Conference and Exposition (DATE 2003), 3-7 March 2003, Munich, Germany, pages 10892-10897. IEEE Computer Society, 2003. Google Scholar
  31. Christian J. Muise, Sheila A. McIlraith, J. Christopher Beck, and Eric I. Hsu. Dsharp: Fast d-DNNF compilation with sharpSAT. In Leila Kosseim and Diana Inkpen, editors, Advances in Artificial Intelligence - 25th Canadian Conference on Artificial Intelligence, Canadian AI 2012, Toronto, ON, Canada, May 28-30, 2012. Proceedings, volume 7310 of Lecture Notes in Computer Science, pages 356-361. Springer, 2012. Google Scholar
  32. Jeho Oh, Paul Gazzillo, and Don S. Batory. t-wise coverage by uniform sampling. In Thorsten Berger, Philippe Collet, Laurence Duchien, Thomas Fogdal, Patrick Heymans, Timo Kehrer, Jabier Martinez, Raúl Mazo, Leticia Montalvillo, Camille Salinesi, Xhevahire Tërnava, Thomas Thüm, and Tewfik Ziadi, editors, Proceedings of the 23rd International Systems and Software Product Line Conference, SPLC 2019, Volume A, Paris, France, September 9-13, 2019, pages 15:1-15:4. ACM, 2019. Google Scholar
  33. David A. Plaisted. History and prospects for first-order automated deduction. In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, volume 9195 of Lecture Notes in Computer Science, pages 3-28. Springer, 2015. Google Scholar
  34. Neha Rungta. A billion SMT queries a day (invited paper). In Sharon Shoham and Yakir Vizel, editors, Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I, volume 13371 of Lecture Notes in Computer Science, pages 3-18. Springer, 2022. Google Scholar
  35. Tian Sang, Paul Beame, and Henry A. Kautz. Performing bayesian inference by weighted model counting. In Manuela M. Veloso and Subbarao Kambhampati, editors, Proceedings, The Twentieth National Conference on Artificial Intelligence and the Seventeenth Innovative Applications of Artificial Intelligence Conference, July 9-13, 2005, Pittsburgh, Pennsylvania, USA, pages 475-482. AAAI Press / The MIT Press, 2005. Available from: URL: http://www.aaai.org/Library/AAAI/2005/aaai05-075.php.
  36. Shubham Sharma, Rahul Gupta, Subhajit Roy, and Kuldeep S. Meel. Knowledge compilation meets uniform sampling. In Gilles Barthe, Geoff Sutcliffe, and Margus Veanes, editors, LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018, volume 57 of EPiC Series in Computing, pages 620-636. EasyChair, 2018. Google Scholar
  37. Carsten Sinz, Andreas Kaiser, and Wolfgang Küchlin. Formal methods for the validation of automotive product configuration data. Artif. Intell. Eng. Des. Anal. Manuf., 17(1):75-97, 2003. Google Scholar
  38. 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):208:1-208:32, 2024. Google Scholar
  39. Zhenghang Xu, Minghao Yin, Jianan Wang, and Jean-Marie Lagniez. A distributed framework for compiling and reasoning with d-dnnf. In Renata Wassermann, Marie-Laure Mugnier, and Franz Baader, editors, Proceedings of the 23rd International Conference on Principles of Knowledge Representation and Reasoning, KR 2026, Lisbon, Portugal. July 20-23, 2026, 2026. Google Scholar
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