Proceedings

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

Armin Biere, Jean-Marie Lagniez, Emmanuel Lonca

Download BibTeX Cite

Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence. Main Track. Pages 3774-3782.

https://doi.org/10.24963/ijcai.2026/420

Keywords

  • Knowledge Representation and Reasoning: Knowledge compilation

Abstract

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.

Armin Biere, Jean-Marie Lagniez, and Emmanuel Lonca. 2026. Efficient Minimization of Decision-DNNF Circuits via Semantic Hashing and Provenance Tracking. In Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-26. IJCAI, 3774–3782. https://doi.org/10.24963/ijcai.2026/420
Welcome Future Conferences AI Journal Division IJCAI Proceedings About IJCAI IJCAI Awards