---
title: "Efficient Minimization of Decision-DNNF Circuits via Semantic Hashing and Provenance Tracking"
authors:
  - "Armin Biere"
  - "Jean-Marie Lagniez"
  - "Emmanuel Lonca"
doi: "10.24963/ijcai.2026/420"
url: "https://ijcai.org/proceedings/2026/420"
pdf: "https://ijcai.org/proceedings/2026/0420.pdf"
venue: "Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence"
year: 2026
pages: "3774-3782"
track: "Main Track"
keywords:
  - "Knowledge Representation and Reasoning: Knowledge compilation"
---

# 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*, pages 3774-3782. DOI: [10.24963/ijcai.2026/420](https://doi.org/10.24963/ijcai.2026/420)

## 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.