2026-07-21T19:26:06Z https://drops.dagstuhl.de/oai

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

decdnnf_rs: A Framework for Querying d-DNNF (Tool Paper) Lagniez, Jean-Marie Lonca, Emmanuel Knowledge compilation d-DNNF Model counting Model enumeration Uniform sampling 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jean-Marie Lagniez and Emmanuel Lonca 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.38 urn:nbn:de:0030-drops-263442 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.38 eng https://creativecommons.org/licenses/by/4.0/legalcode