Efficient Minimization of Decision-DNNF Circuits via Semantic Hashing and Provenance Tracking

Efficient Minimization of Decision-DNNF Circuits via Semantic Hashing and Provenance Tracking

Armin Biere, Jean-Marie Lagniez, Emmanuel Lonca

Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence
Main Track. Pages 3774-3782. https://doi.org/10.24963/ijcai.2026/420

Knowledge Compilation transforms propositional formulas into tractable structures like decision-DNNF to support efficient reasoning. However, these representations often suffer from exponential size, and standard minimization via SAT sweeping is computationally prohibitive for large instances. In this paper, we propose a scalable minimization framework for decision-DNNF that eliminates the need for SAT solvers. We introduce a semantic hashing technique leveraging polynomial-time model counting to rapidly filter redundancies, followed by a polynomial-time verification strategy based on CNF projection. Our experimental evaluation demonstrates that this approach efficiently compresses decision-DNNF circuits while avoiding the bottleneck of NP-hard equivalence checks.
Keywords:
Knowledge Representation and Reasoning: Knowledge compilation