literal. 

Definition 4. An OBDD-L is *reduced* (ROBDD-L) if 1. No two distinct nodes u and v have the identical variable, implied literals, low child and high child; 2. No node has two identical children; Definition 5. Given a number 0 ≤ i ≤ ∞, a OBDD-L precisely has i implied literals (OBDD-i) if (1) each node v has i implied literals, or (2) j (j < i) implied literals and L(v) = L∞(v). A ROBDD-i is a reduced OBDD-i. 

Particularly, OBDD-∞ is also called "OBDD with as many implied literals as possible". It is obvious that ROBDD-0 is isomorphic to ROBDD. By Proposition 1, we have that L(v) = L∞(v) for any node v in OBDD-∞, then the False node does not appear in any OBDD-∞. 

Figure 2 are a ROBDD-0 and a ROBDD-1 about the formula (x1 ↔ y1) ∧ (x2 ↔ y2) over the variables order x1
< x2 < y1 < y2. The nodes in ROBDD-0 are obviously less than those in ROBDD-1. Furthermore, all the ROBDDs-i
(i > 0) presenting this formula over the same variables order are the same. If this formula is extended to (x1 ↔ y1) 
∧ … ∧ (xn ↔ yn) over x1 < … < xn < y1 < … < yn, then ROBDD-0 will have more than 2n + 1 nodes, while the number of nodes in ROBDD-i (i > 0) is 2n + 1. 

![0_image_0.png](0_image_0.png)

Figure 2. An example about ROBDD-0 (left) and ROBDD-1 It is well known that for any formula there is exactly one ROBDD representing it. We will show that for any 0 
≤ i ≤ ∞, ROBDD-i also has this property. First, we give the definition of Condition [3, 5], which is a useful logical operation in practical applications. Note that we do not restrict this definition to the NNF formulas here. 

Definition 6. Let ϕ be a formula over the variables set X and let T be a consistent term. The conditioning of ϕ on T (denoted by ϕ | T, simply denoted by ϕ | l if T = {l}) is a formula obtained by replacing every variable x in ϕ with *true* (resp. *false*) if x ∈ T (resp. ¬x ∈ T). 

Given any formula ϕ, variable x, literal l and consistent term T, by Theorem 1 in [3], we have that: ϕ ⇔ (ϕ | l) 
∧ l if ϕ ⇒ l; ϕ ⇔ ϕ | x if ϕ | x ⇔ ϕ | ¬x (we say x can be *omitted* in ϕ). Given two equivalent formulas ϕ1 and ϕ2, all variables do not appear in both ϕ1 and ϕ2 can be omitted. And given an OBDD-L with root v, according to (*), 
φ(v) | L(v) ∪ ¬var(x) (resp. φ(v) | L(v) ∪ var(x)) is equivalent to φ(lo(v)) (resp. φ(hi(v))). These observations are used in the proofs of many propositions in this paper, including the following conclusion. 

Proposition 2. For any formula ϕ over the set of variables X = {x1, … , xn} with the linear order x1 < … < xn, and any 0 ≤ i ≤ ∞, there is exactly one ROBDD-i to represent ϕ. 

Proof. By induction on the size of X. The case | X | = 0 is obvious. Assume now that we have proven this proposition for | X | ≤ n. We proceed to show it for | X | = n + 1. 

First we show that there exists some ROBDD-i equivalent to ϕ. By the induction hypothesis, this assertion is obvious if there exists some variable x ∈ X that can be omitted in ϕ. Otherwise, we construct a ROBDD-i equivalent to ϕ (In fact, it is just the idea of the compilation algorithm Build, see Section 5). Let {l1, … , lm} be the set of literals implied by ϕ such that the variable of lj is less than the one of lj′ if j < j′, let L(v) = {l1, … , lm′}, where m′ = min{m, i}. If there does not exist any variable appearing in ϕ but not in L(v), then 〈L(v)〉 is equivalent to ϕ. Otherwise let var(v) be the minimum variable appearing in ϕ but not in L(v). It is obvious ϕ | L(v) ∪ {¬x} is not equivalent to ϕ | L(v) ∪ {x}. By the induction hypothesis, the ROBDDs-i corresponding to ϕ | L(v) ∪ {¬x} and ϕ | L(v) ∪ {x} are not identical to each other, and let lo(v) and hi(v) be their roots, respectively. It is obvious that the DAG with the root v is a ROBDD-i such that φ(v) is equivalent to ϕ. 

Then assume that there exist two ROBDDs-i with the roots u and v for ϕ, we prove that they are identical to each other. It is obvious that L(u) = L(v) by Proposition 1 and the definition of ROBDD-i. And if var(u) ≠ var(v), without loss of generality we assume that var(u) < var(v), this means that var(u) can be omitted in ϕ, then the 