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

1 Introduction

Propositional logic serves as a cornerstone of Artificial Intelligence, providing a rigorous approach to knowledge representation and reasoning [Brachman and Levesque, 2004]. It underpins critical AI subfields, including Explainable AI (XAI) [Darwiche, 2023], automated reasoning [Biere et al., 2021], and decision support systems [Plaisted, 2015]. However, expressiveness of propositional logic comes at a computational cost: core inference tasks, such as satisfiability (SAT), are NP-hard [Cook, 1971]. This inherent complexity of SAT solving creates a bottleneck for real-time applications, particularly in high-stakes environments where latency and accuracy are non-negotiable.

Industrial applications exacerbate this challenge, demanding scalability for massive problem instances. For example, AWS's Zelkova engine [Rungta, 2022] processes billions of verification queries daily, highlighting the urgent need for optimized reasoning pipelines [Biere et al., 2021]. To mitigate on-line computational costs, Knowledge Compilation (KC) has emerged as a standard paradigm [Cadoli and Donini, 1997; Darwiche and Marquis, 2002]. KC shifts the computational burden to an off-line phase, compiling propositional formulas into target languages that support polynomial-time querying. Prominent among these is the Decision-DNNF (decision-DNNF), which renders tasks like Weighted Model Counting (WMC) tractable. The practical utility of this approach is evident in systems like Renault's configuration tool [Astesana et al., 2010], where precomputed compilations enable rapid product customization.

Nevertheless, Knowledge Compilation is not a panacea; it trades time complexity for space complexity. While decisionDNNF circuits facilitate efficient inference, they are susceptible to exponential blow-up in size, which severely hampers scalability and storage efficiency [Bova et al., 2016]. This 'tractability-vs-size' trade-off presents a significant barrier to deploying KC in resource-constrained or large-scale scenarios. Consequently, minimizing these compiled representations is a critical post-processing step. State-of-the-art reduction frameworks, such as those inspired by FRAIGs (Functionally Reduced And-Inverter Graphs), typically rely on SAT sweeping [Biere et al., 2024b; Amar`u et al., 2020; Kuehlmann, 2004; Lu et al., 2003]. This process involves incrementally solving a sequence of topologically ordered SAT problems to identify and merge functionally equivalent nodes. However, a major bottleneck of this approach is the sheer volume of solver calls required, which becomes computationally prohibitive for large circuits.

In this paper, we propose a novel minimization framework that avoids expensive SAT calls by exploiting the inherent properties of the target language itself. Our key insight is that since decision-DNNF representations allow for polynomialtime model counting, we can leverage semantic information (specifically model counts) to accelerate equivalence checking. We introduce a specialized hashing mechanism that utilizes the model count and the variable set of each node as a semantic signature. Unlike pure structural hashing, this hybrid approach integrates both combinatorial and numerical properties to efficiently identify candidate sub-circuits for merging. By computing these signatures, we can rapidly cluster structurally similar components and drastically reduce the search space for equivalence testing.

Furthermore, we supplant the traditional SAT-based verification step with a polynomial-time refinement process. We achieve this by tagging the decision-DNNF structure with metadata derived from the original CNF formulas. These CNF-based annotations allow us to trace the provenance of sub-circuits and thus verify logical equivalence through a polynomial structured check, ensuring correctness without reverting to full NP-hard reasoning.

Our contributions can be summarized as follows: we propose a specialized hashing function for decision-DNNF minimization that utilizes model counts and variable sets to detect functional redundancy. Additionally, we introduce a polynomial-time verification strategy leveraging CNF-based annotations, which eliminates the need for SAT sweeping. Finally, we demonstrate that this approach significantly reduces circuit size while strictly preserving all semantic properties.

Section 2 introduces the necessary notation. Section 3 details our minimization framework, combining semantic hashing with polynomial-time verification. We discuss related work in Section 4 and present our experimental results in Section 5. Finally, Section 6 concludes the paper.

2 Formal Preliminaries

We consider a propositional language L defined over a finite set of variables X . A literal is a variable x ∈ X or its negation ¬x. For a literal ℓ, Var(ℓ) denotes the underlying variable. A formula Σ is constructed using standard logical connectives (∧, ∨, ¬) and the logical constants ⊤ (true) and ⊥ (false). Var(Σ) denotes the set of variables appearing in Σ.

Semantics are defined as usual. An assignment ω is a mapping ω : X → {0, 1}. We often view an assignment ω as the set of literals it satisfies. Under this interpretation, we can apply standard set-theoretic operations (e.g., intersection, union) to assignments. Given a subset of variables X ⊆ X, ω[X] denotes the projection of the assignment onto X.

We say ω satisfies Σ, denoted ω |= Σ, if Σ evaluates to 1 under ω. The set of all satisfying assignments (or models) of Σ is denoted by Mod(Σ). If Mod(Σ) = ∅, the formula is unsatisfiable (or inconsistent), denoted as Σ ≡ ⊥. Two formulas Σ1 and Σ2 are equivalent, denoted Σ1 ≡ Σ2, iff Mod(Σ1) = Mod(Σ2). Finally, Σ1 implies Σ2, denoted Σ1 |= Σ2, iff Mod(Σ1) ⊆Mod(Σ2).

A Conjunctive Normal Form (CNF) formula is a conjunction of clauses, where each clause is a disjunction of literals. We view a CNF Σ as a set of clauses, and a clause as a set of literals. The conditioning of Σ by a literal ℓ, denoted Σ|ℓ, is obtained by replacing every occurrence of ℓ with ⊤ and every occurrence of its negation ¬ℓ with ⊥. This is followed by standard Boolean simplifications (e.g., removing clauses satisfied by ⊤ and removing ⊥ from clauses) until the formula is minimal. This notion extends to a set of literals S = {ℓ1, . . . , ℓm} by iterative application:

Example 1. Consider the following CNF formula Σ with four clauses defined over the variables X = {x1, . . . , x5}:

Conditioning Σ on x1 satisfies the last three clauses with x1 and simplifies the first clause (removing ¬x1), yielding:

We further consider formulas in deterministic Decomposable Negation Normal Form (d-DNNF), which are represented by a rooted Directed Acyclic Graph (DAG) where leaves are literals or constants, and internal nodes are either decomposable AND gates or deterministic OR gates [Darwiche, 2002]. Decomposability requires that for any AND node, the variable sets of its children are disjoint. Determinism requires that for any OR node, the children are mutually inconsistent (disjoint models).

In this work, we focus on a specific subset of d-DNNF known as decision-DNNF [Huang and Darwiche, 2005] (also referred to as Decomposable Decision Graphs [Fargier and Marquis, 2006]). In a decision-DNNF, the logical structure is defined by decision nodes. A decision node N is of the form ite(x,N⊤,N⊥), representing "if x then N⊤ else N⊥". Semantically, this is equivalent to (x∧N⊤)∨(¬x∧N⊥). To strictly adhere to the d-DNNF properties we assume:

• Decomposability: The decision variable x must not appear in the sub-circuits rooted at N⊤ or N⊥.
• Determinism: Guaranteed by the structure, as x and ¬x are mutually exclusive.

Modern compilers like d4 [Lagniez and Marquis, 2017a], SharpSAT-TD [Kiesel and Eiter, 2023], Dsharp [Muise et al., 2012] and C2D [Darwiche, 2004] typically output this format. The size of a decision-DNNF, denoted |Σ|, is the number of edges in the graph.

To facilitate the presentation of our reduction rules, we assume each node in the decision-DNNF is associated with a unique index i, denoted as Ni. We define the following properties for any given node Ni:

• Var(Ni): The set of variables in the scope of the subcircuit rooted at Ni.
• Lits(Ni): The set of literals (decisions) encountered on the path from the root to Ni. In cases where Ni appears as a child of both branches of a decision node, the negative literal is systematically selected.
• circ(Ni): The structural sub-circuit rooted at Ni.
• mc(Ni): The model count of circ(Ni), i.e., the number of satisfying assignments over Var(Ni).

A key advantage of decision-DNNFs is that mc(Ni) can be computed in linear time via a bottom-up traversal:

• If Ni is a literal or ⊤, mc(Ni) = 1. If Ni is ⊥, mc(Ni) = 0.
• For a decision node Ni = ite(x,N⊤,N⊥), the count is the sum of its children: mc(Ni) = mc(N⊤)+mc(N⊥). (This assumes the circuit is smooth, meaning N⊤ and N⊥ cover the same set of variables).
• For an AND node Ni = ∧(Nj1 , . . . ,Njk ), the count is the product of its children: mc(Ni) = ∏km=1 mc(Njm ).

Example 2 (Example 1 cont'ed). Figure 1 depicts a valid decision-DNNF, denoted Ψ, representing the CNF formula Σ. The size of this circuit is |Ψ| = 18. The model count of the root node corresponds to the count of the entire formula: mc(N0) = mc(Σ) = 23. We can observe specific properties for internal nodes:

• Variables: Nodes N3 and N5 share the same variable scope: Var (N3) = Var (N5) = {x2, x3}.

• Model Counts: Nodes N3 and N5 exhibit identical model counts: mc(N3) = mc(N5) = 3.
• Path Literals: Nodes N3 and N5 are reached via different paths. N3 is reached via the high branch of x1 and low branch of x4, so Lits(N3) = {x1, ¬x4}. Conversely, N5 is reached via the low branch of x1, so Lits(N5) = {¬x1}.

3 ProposedMinimization Framework

Our objective is to minimize a decision-DNNF Ψ by merging functionally equivalent sub-circuits. Let Ni and Nj be two nodes in Ψ. We say Ni ≡ Nj if the Boolean functions represented by the sub-circuits rooted at Ni and Nj are logically equivalent, i.e., circ(Ni) ≡ circ(Nj). A naive approach would perform a quadratic number of equivalence checks using a SAT solver, which is intractable. Instead, we propose a scalable two-phase strategy consisting of Semantic Hashing, a constant-time heuristic filter to identify candidate pairs, followed by CNF-Based Verification, a polynomial-time determinization step leveraging the original CNF Σ.

3.1 Semantic Hashing

The first phase rapidly filters obvious non-equivalences using a semantic signature. Given the properties of decisionDNNFs defined in Section 2, two equivalent nodes must necessarily share the same variable scope and the same model count. We define the semantic hash of a node Ni as a tuple:

Before identifying candidate pairs, we compute H(Ni) for all nodes in a single bottom-up pass. If H(Ni) ̸= H(Nj), then Ni ̸≡ Nj. This acts as a powerful pruning metric: matching model counts is a strong indicator of potential equivalence, drastically reducing the search space compared to purely "structural hashing" (cf. [Biere et al., 2024a]), which misses semantically equivalent but structurally different graphs.

Example 3 (Example 1 continued). Revisiting the decisionDNNF depicted in Figure 1, we observe that nodes N3 and N5 share identical signatures:

Thus they are identified as a candidate pair for equivalence and grouped into the same bucket for subsequent verification.

3.2 Verification via CNF Projection

While H(Ni) = H(Nj) is a necessary condition for equivalence, it is not sufficient (collisions can occur). To verify equivalence without invoking a SAT solver, we leverage the provenance of the circuit - specifically, the original CNF formula Σ from which Ψ was compiled. The core idea is to associate each node Ni with a specific fragment of Σ that precisely defines the logic of that sub-circuit.

Conditioning by Path Literals. Any node Ni operates within a context defined by the path literals Lits(Ni) from the root. Intuitively, conditioning the original formula Σ by these literals restricts the global function to the specific branch currently traversed. However, a scope mismatch arises: while the sub-circuit Ni is defined strictly over Var(Ni), the conditioned formula Σ|Lits(Ni) remains defined over all variables not assigned on the path - including those belonging to parallel branches (siblings). Consequently, Σ|Lits(Ni) does not correspond solely to Ni, but rather to the conjunction of Ni and the constraints imposed by all sibling sub-circuits encountered on the path.

Proposition 1 (Conditioned Equivalence). Let Σ be a CNF formula represented by a decision-DNNF Ψ. For any node Ni, let π be the path from the root to Ni defined by Lits(Ni). We define the set of path-relevant nodes, denoted K(π), as the union of {Ni} and the set of all siblings of AND nodes appearing on π. Then:

Proof. We proceed by induction on the length of the path π from the root N0 to Ni.

Base Case: The path is empty (length 0), so Ni = N0 (the root). Here, Lits(N0) = ∅. The set K(π) = {N0} (no ancestors, so no siblings). The statement reduces to Σ ≡ circ(N0), which holds by the definition of the circuit representing Σ.

Inductive Step: Assume that for a node P with path πP , we have:

Let C be a child of P. We distinguish two cases depending on the type of P:

Case 1: P is a Decision Node (P = ite(x, P⊤, P⊥)). Assume w.l.o.g. that C = P⊤. The path πC extends πP with the decision literal x. Thus, Lits(C) = Lits(P) ∪ {x}. The set of relevant nodes remains unchanged except replacing P with C (no AND siblings added), so conceptually K(πC) ≡ K(πP ) \ {P} ∪ {C}. From the hypothesis: Σ|Lits(P) ≡ P ∧Φrest, where Φrest are the ancestor siblings. Conditioning on x:

Since P |x ≡ P⊤ = C (by definition of ITE), and Φrest does not depend on x, we get Σ|Lits(C) ≡ C∧Φrest. This matches the conjunction over K(πC).

Case 2: P is a Decomposable AND Node (P = C ∧ S). Here, C is the child we traverse, and S is the sibling. The path πC extends πP but adds no new literals (AND nodes are not decisions), so Lits(C) = Lits(P). However, the structure changes: P decomposes into C ∧ S. The set K(πC) now includes the new sibling S. From the hypothesis:

Substituting P ≡ C ∧ S:

This is exactly the conjunction of the current node (C), the new sibling (S), and previous siblings (Φrest), which corresponds to ∧Nj∈K(πC) circ(Nj).

Conclusion: By induction, the proposition holds for all nodes reachable from the root.

Example 4 (Example 1 continued). Revisiting the decisionDNNF depicted in Figure 1, consider the path defined by ¬x1, we have: Σ|¬x1 ≡ circ(N5) ∧ circ(N6).

Due to the decomposable nature of AND nodes in Ψ, variables outside Var (Ni) typically belong to sibling sub-circuits and should not influence the equivalence of circ(Ni). In the following, we show how to pinpoint the exact CNF fragment equivalent to circ(Ni).

Clause Separation Property. To isolate the logic of Ni, we must filter Σ|Lits(Ni) to retain only clauses relevant to Var(Ni). We rely on the following property of decomposable representations:

Proposition 2 (Decomposable Clause Separation). Let Σ be a CNF formula representing a function f. Assume f decomposes into f(A) ∧ f(B) where A and B are disjoint sets of variables. If clause α ∈ Σ can be written as α = β1 ∨β2 with Var (β1) ⊆ A and Var (β2) ⊆ B, then Σ |= β1 or Σ |= β2.

Proof. First, if Σ is unsatisfiable, the proposition holds vacuously. Assume Σ is satisfiable. To proceed by contradiction, suppose that: Σ ̸|= β1 and Σ ̸|= β2. This implies there exist models ω1 and ω2 such that:

Since Σ ≡ f (A) ∧ f (B), any model of Σ must satisfy both projected components:

Because A ∩ B = ∅, we can construct a new assignment ω by combining the relevant parts of ω1 and ω2:

This assignment is well-defined and as we have

it follows that ω |= f(A) ∧ f(B), and therefore ω |= Σ.

However, consider the clauses β1 and β2:

• Since Var(β1) ⊆ A, the truth value of β1 under ω depends only on assignments in A. As ω1 |= ¬β1 and ω[A] = ω1[A], we have ω |= ¬β1.
• Similarly, since Var(β2) ⊆ B, the truth value depends only on B. As ω2 |= ¬β2 and ω[B] = ω2[B], we have ω |= ¬β2.

Consequently, we derive ω |= ¬β1 ∧ ¬β2, which implies ω |= ¬(β1 ∨ β2), or ω |= ¬α.

Contradiction: We have established that ω |= Σ. Since α ∈ Σ, every model of Σ must satisfy α. However, we showed that ω |= ¬α.

Example 5 (Example 1 continued). Let us consider again the decision-DNNF depicted in Figure 1. Let us consider the formula Σ|¬x1 = {x2 ∨ x3, x3 ∨ x4 ∨ x5, ¬x3 ∨ x4 ∨ x5}.

This proposition implies that when a clause is shared between two sub-circuits linked by an AND node, it must functionally belong to one side or the other (or be tautological). Based on this, we define the Local CNF of a node Ni given a CNF formula Σ, denoted cnf (Ni, Σ), as the subset of conditioned clauses projected onto the node's variables, retaining only those strictly entailed by the sub-circuit:

Example 6 (Example 1 continued). Revisiting the decisionDNNF shown in Figure 1, consider the conditioned formula: Σ|¬x1 = {x2∨x3, x3∨x4∨x5, ¬x3∨x4∨x5}. The local CNF projections for the sub-circuits are: cnf (N5, Σ) = {x2 ∨x3} and cnf (N6,Σ) = {x4 ∨ x5}. This illustrates the projection property, as the full conditioned formula entails the local clauses (e.g., Σ|¬x1 |= x4 ∨ x5).

In fact, the following corollary states that the local CNF projection is logically equivalent to the sub-circuit itself.

Corollary 1. Let Σ be a CNF formula represented by a decision-DNNF Ψ and Ni a node of Ψ, then circ(Ni) ≡ cnf (Ni, Σ).

Proof. By Proposition 1, we have that

where circ(Ni) and Φrest do not share any variables. We verify that this corresponds to cnf (Ni,Σ) ∧ cnf (Φrest,Σ) by considering any clause α ∈ Σ|Lits(Ni). If Var(α) ⊆ Var(Ni), then α ∈ cnf (Ni,Σ). If Var(α) ⊆ Var(Φrest), then α ∈ cnf (Φrest,Σ). If Var(α) is shared between Ni and Φrest, then by Proposition 2, this clause can be split into two parts α = βNi ∨ βΦrest . If circ(Ni) |= βNi then βNi ∈ cnf (Ni,Σ), and if Φrest |= βΦrest then βΦrest ∈ cnf (Φrest,Σ). Since Σ|Lits(Ni) ≡ circ(Ni) ∧ Φrest ≡ cnf (Ni,Σ) ∧ cnf (Φrest,Σ) and Var(Ni) = Var(cnf (Ni, Σ)) and Var(Φrest) = Var(cnf (Φrest, Σ)), it follows that circ(Ni) ≡ cnf (Ni, Σ).

Algorithm 1: decision-DNNF Minimization

// 1. Semantic Hashing 1 Compute H(u) = ⟨Var (u), mc(u)⟩ ∀u ∈ Ψ; 2 Buckets ← Group nodes u by value of H(u); // 2. Verification and Merging 3 foreach bucket B ∈ Buckets such that |B| > 1 do 4 while B ̸= ∅ do 5 u ← Pop(B) ; // Select pivot 6 foreach v ∈ B do // Check Mutual Entailment 7 if circ(u) |= cnf (v, Σ) and circ(v) |= cnf (u,Σ) then 8 Merge(v, u); 9 B ← B \ {v};

10 return Ψ;

Finally, to verify if two candidate nodes Ni and Nj (where H(Ni) = H(Nj)) are equivalent, it is possible to take advantage of the following proposition.

Proposition 3. Let Σ be a CNF formula represented by a decision-DNNF Ψ. Let N1 and N2 be two nodes of Ψ. If circ(N1) |= cnf (N2,Σ) and circ(N2) |= cnf (N1,Σ), then circ(N1) ≡ circ(N2).

Proof. Corollary 1 implies that circ(N1) ≡ cnf (N1, Σ) and, likewise, that circ(N2) ≡ cnf (N2,Σ). Thus, if circ(N1) |= cnf (N2,Σ) then circ(N1) |= circ(N2), and if circ(N2) |= cnf (N1,Σ) then circ(N2) |= circ(N1). Consequently, circ(N1) ≡ circ(N2).

Because clause entailment can be decided in polynomial time for decision-DNNF [Darwiche and Marquis, 2002], computing this projection is tractable. Notably, this tractability extends to the broader class of DNNFs as well. Therefore, it is possible to verify if circ(Ni) |= cnf (Nj,Σ) in polynomial time. By performing this check in both directions (mutual entailment), we can determine the equivalence of two sub-circuits efficiently.

Algorithm 1 provides a detailed summary of the proposed minimization framework. The procedure begins by computing the semantic hash H(u) for every node in a bottom-up pass (line 1). Nodes sharing the same hash are grouped into buckets, representing potential equivalence classes (line 2). The algorithm then iteratively refines these buckets. For each bucket, it selects a representative pivot u and compares other candidates v against it (lines 6-10). To verify equivalence, it checks if the pivot sub-circuit circ(u) entails the Local CNF of the candidate cnf (v, Σ) (and vice-versa). If this mutual entailment holds (Line 7), the nodes are confirmed to be equivalent; consequently, v is merged into u (line 8), and v is removed from the bucket (line 9).

It is important to note that the decision-DNNF produced by Algorithm 1 is minimal in the sense that no two distinct sub-circuits represent equivalent Boolean functions.

Proposition 4 (Minimality). Let Ψ′ be the decision-DNNF returned by Algorithm 1. For any two distinct nodes Ni, Nj ∈ Ψ′ , circ(Ni) ̸≡ circ(Nj).

Proof. We proceed by contradiction. Assume there exist two distinct nodes Ni,Nj in Ψ′ such that circ(Ni) ≡ circ(Nj). Since the nodes are equivalent, they must share the same variable scope and model count (as established in Section 3.1). Thus, H(Ni) = H(Nj), meaning both nodes were initially placed in the same bucket B during Phase 1.

Consider the iteration of the While loop (Line 6) where the first of these two nodes, say Ni, is selected as the pivot u. At this moment, since Nj is distinct and has not yet been processed as a pivot, it must be present in B (or have been merged into an equivalent node Nk, which would transitively imply Ni ≡ Nk). The algorithm then performs the mutual entailment check between u = Ni and v = Nj (Line 9). Since we assumed circ(Ni) ≡ circ(Nj), by the previous Proposition, the conditions circ(Ni) |= cnf (Nj,Σ) and circ(Nj) |= cnf (Ni,Σ) are satisfied. Consequently, Nj is merged into Ni (Line 10) and removed from the bucket. Therefore, Nj cannot appear as a distinct node in the final output Ψ′ , which contradicts the assumption.

4 RelatedWork

Complexity of Knowledge Compilation. Despite the inferential tractability of d-DNNF, the size of compiled circuits remains a critical bottleneck. Theoretical results have established unconditional lower bounds for knowledge compilation languages, proving that succinct representations for general propositional theories are infeasible under standard complexity assumptions [Bova et al., 2016; Beame et al., 2017].

Consequently, d-DNNF circuits often exhibit exponential growth relative to the input formula size. While heuristic optimizations exist [Koriche et al., 2013], they typically target specific sub-classes or lack a systematic approach to postcompilation minimization. Our work operates within these theoretical bounds but seeks to minimize the practical representation size of tractable instances.

Circuit Minimization and FRAIGs. In the broader field of logic synthesis, AND-Inverter Graphs (AIGs) serve as a standard representation for boolean networks [Kuehlmann et al., 2002]. To optimize these structures, the Functionally Reduced AIG (FRAIG) framework was developed, integrating structural hashing with SAT-based functional reduction [Mishchenko et al., 2005].

The core mechanism of FRAIGs involves identifying potentially equivalent nodes via simulation and verifying their equivalence using a SAT solver (SAT sweeping). This approach is widely used in hardware verification and equivalence checking [Goldberg et al., 2001; Biere, 2021].

Since d-DNNFs are essentially Boolean circuits, FRAIGstyle reduction is theoretically applicable. However, the reliance on SAT sweeping introduces a severe computational bottleneck. Confirming the equivalence of cut-points requires repeated calls to an NP-complete oracle, which contradicts the goal of using compiled languages (like d-DNNF) specifically designed to avoid such complexity.

In contrast, our approach replaces the expensive SAT solver with a polynomial-time semantic hash based on model counting, leveraging the inherent properties of the d-DNNF itself to facilitate efficient equivalence checking.

Redundancy in Knowledge Compilation. Specific to the d-DNNF context, recent work has addressed size reduction by targeting artifacts introduced during compilation. Notably, compilers that rely on Tseitin transformations introduce auxiliary variables that may become redundant during downstream tasks. Kiesel et al. [Kiesel and Eiter, 2023] and Derkinderen [Derkinderen, 2024] demonstrated that when these variables are existentially quantified (projected out), the resulting circuits often contain large tautological substructures. Derkinderen proposed a bottom-up traversal to detect and prune these artifacts efficiently.

While effective, this technique is limited in scope: it primarily addresses redundancies arising from forgetting (existential quantification). It does not address general functional redundancies in standard compilation scenarios where variables are preserved. Our method generalizes this minimization objective, identifying functional equivalence across arbitrary sub-circuits regardless of their origin.

Equivalence of two decision-DNNFs. It is currently unknown whether the equivalence of two arbitrary decisionDNNFs can be decided in polynomial time; the question remains open [Darwiche and Marquis, 2002]. However, randomized algorithms allow for equivalence checking with high statistical confidence. This strategy is based on the arithmetization method originally proposed for FBDDs (a subclass of decision-DNNFs without decomposable AND nodes) in [Blum et al., 1980]. The key insight is to transform the circuit into a multilinear polynomial over a finite field and evaluate it at a random assignment. If the computed values differ, the circuits are definitely not equivalent; if they match, they are equivalent with high probability.

Since the detection of non-equivalence is always certain, the non-equivalence problem belongs to the complexity class RP, placing the equivalence problem in co-RP. As shown in [Darwiche and Huang, 2002], this technique extends effectively to decision-DNNFs. In contrast to our work, which provides a deterministic check by leveraging the source CNF, this method is probabilistic. Furthermore, to the best of our knowledge, no minimization algorithm leveraging this randomized check has been developed to date.

5 Experimental Evaluation

Since there are no existing complete reduction algorithms specifically designed for decision-DNNFs, we evaluate our technique against FRAIG. We integrated our algorithm into the decdnnf rs reasoner [Lagniez and Lonca, 2024; Lonca and Lagniez, 2026] and performed comparisons using the FRAIG implementation in abc, executed via the &fraig -y command. 1 Detailed logs and experimental artifacts are available at https://zenodo.org/records/20165767.

We compared both approaches using 3,828 benchmarks drawn from recent studies. First we considered 940 instances from enumeration studies [Spallitta et al., 2024] divided into four sets: Binary Clauses (binary - 50 instances), random 3-SAT problems (rnd3sat - 410 instances), Random-3SAT Instances with Controlled Backbone Size (CBS - 1000 instances), and Random-3-SAT Instances and Backboneminimal Subinstances (BMS - 500 instances); Then we used 246 instances from three recent model counting competitions (https://mccompetition.org), 197 from [Lagniez and Marquis, 2017b] to evaluate d4 and 1425 benchmarks from studies on uniform sampling [Sharma et al., 2018; Lagniez and Lonca, 2025].

1 https://github.com/berkeley-abc/abc, commit c18b9a2

We employed d4 2 to compile the source CNF benchmarks into decision-DNNF representations. For our evaluation, we restricted the dataset to the 3,596 benchmarks where compilation completed successfully within a one-hour timeout and the resulting formula was satisfiable (i.e., admitted at least one model). Experiments were conducted on machines equipped with Intel ® Xeon ® E5-2637 v4 CPUs and 50 GB of RAM, running Rocky Linux 9.5.

To facilitate comparison with FRAIG, we developed an utility to translate decision-DNNFs into ASCII AIG format, which were subsequently converted to binary AIGs using the aigtoaig tool from the AIGER suite [Biere, 2007; Biere et al., 2011]. While FRAIG leverages this optimized binary input, decdnnf rs currently processes the circuit structure directly, as it does not yet support a native binary format.

Translating decision-DNNFs produced by d4 into AIGs can significantly increase the number of conjunction nodes as, to ensure succinctness, d4 employs an edge-labeled representation where literals are associated with edges rather than nodes. In this format, literals on an edge represent assignments that must be propagated during path traversal.

This compact encoding allows, for example, a term of arbitrary length to be represented by just two nodes and a single labeled edge. Conversely, the AIG format is restricted to binary conjunctions, requiring n-1 nodes to represent a term of n literals. While this translation introduces nodes not present in the original decision-DNNF, many are redundant and can be merged via structural hashing when the instance is loaded by abc, prior to the application of FRAIG.

The reduction in node count through initial structural hashing is considered negligible in our analysis. This is justified by two factors: (i) the process primarily merges nodes that are artifacts of the AIG translation and were not present in the original decision-DNNF structure; and (ii) computational overhead of structural hashing (including I/O) is small, i.e., less than one second per average, peaking at 57 seconds, thus a negligible fraction of the 3,600 seconds time budget. Both decdnnf rs and FRAIG were executed under the same timeout and resource constraints as the initial compilation phase.

We first analyze the CPU time required by each tool to perform circuit reduction, with the results summarized in Fig. 2. The scatter plot reveals that decdnnf rs achieves significantly lower computation times than FRAIG, a result that aligns with the tools' respective theoretical complexities.

Notably, decdnnf rs successfully processed a higher number of instances (3,540) within the timeout compared to FRAIG (3,341). Furthermore, on the subset of benchmarks completed by both approaches, decdnnf rs required an average of only 3.06 s, whereas FRAIG averaged 29.23 s.

2 https://www.cril.univ-artois.fr/software/d4/

Next, we evaluate the reduction efficiency of decdnnf rs compared to FRAIG. Figure 3 illustrates these results by plotting the ratio of eliminated edges for each instance. For our approach, the reduction is measured directly by comparing the edge count before and after the process. For FRAIG, we utilize the ps command in abc to retrieve the number of AIG nodes, noting that the edge count is exactly twice the node count. In Fig. 3, instances where a timeout occurred for decdnnf rs or FRAIG are plotted along the leftmost or bottommost axes, respectively; this signifies that no reduction was successfully computed by that tool, while the competing approach may have completed.

The reduction analysis confirms the superior performance of the decdnnf rs tool over FRAIG. On average, decdnnf rs achieves a reduction of 5.00%, whereas FRAIG yields only 0.68%. Interestingly, all instance families benefit from the reduction provided by decdnnf rs, with average gains ranging from 2.87% for binary instances to 6.65% for competition instances. In contrast, FRAIG fails to find any reduction for the binary family, and its highest average reduction (0.91%) is observed for the rnd3sat instances.

In theory, translating the reduced AIGs back into decdnnf rs representations would allow for a more direct comparison of reduction efficiency. However, this approach is impractical for two primary reasons: (i) there is no guarantee that the circuit produced by the FRAIG command preserves the determinism property required for a valid decdnnf rs; and (ii) it would be necessary to ensure that all auxiliary conjunction nodes introduced during the initial AIG

Figure 3: Comparison of the reduction achieved by decdnnf rs and FRAIG respectively. Each point represents an instance and gives the reduction ratio between the number of edges after and before the reduction with decdnnf rs on the x-axis and FRAIG on the y-axis (higher is better). Timeouts count as no reduction (points on axis).

translation are eliminated, rather than remaining as structural artifacts that would artificially inflate the final edge count.

6 Conclusion and Perspectives

In this paper, we proposed a novel framework for minimizing decision-DNNFs. Our approach leverages a dedicated semantic hashing technique to significantly prune the search space of candidate node pairs. Crucially, by exploiting the relationship between a circuit and its source CNF formula, we introduced a verification method based on local CNF projection, which enables polynomial-time equivalence checking.

We formally proved the resulting circuits to be minimal, in the sense that no two distinct sub-circuits represent the same Boolean function. Our experimental evaluation demonstrates that our minimization process is highly efficient, achieving up to a 10% reduction in edge count on standard benchmarks.

For future work, we plan to investigate whether this minimization framework can be extended to unconstrained dDNNFs. We also aim to integrate this procedure directly into the compilation pipeline; by applying minimization dynamically (potentially via a dedicated parallel thread) we can significantly reduce the memory footprint of intermediate structures and mitigate memory exhaustion on challenging instances. Furthermore, we intend to incorporate probabilistic equivalence tests as an efficient early-rejection filter to quickly prune non-equivalent candidates before performing the full CNF-based verification. Finally, we will further exploit parallelism within the reduction algorithm itself by processing node buckets and equivalence checks concurrently to enhance overall scalability.

Acknowledgements

This work was partly supported by the ANR CERADOC project (ANR-25-CE23-3078). We also thank the anonymous reviewers for their insightful feedback and constructive suggestions.