Proposition 6. Given any formula ϕ over the variables x1 < … < xn and 0 < i ≤ ∞, if ϕ ⇒ C does not hold for any non-tautology clause such that xn does not appear in it, then we have that: all of the ROBDD-i corresponding to ϕ are the same; assume that ROBDD-i has the root v and ROBDD has the root u, then | |1 | | 2 | | 5 2 u v u ⎡ ⎤ − ≤ ≤⋅ − ⎢ ⎥ ⎢ ⎥ . 

Proof. The case ϕ = *false* is impossible. Given any non-terminal node v1 in ROBDD-1, we have that L∞(v1) 
has no other literal except xn and ¬xn, otherwise there exists some literal l such that l ∉ {xn, ¬xn} and ϕ ∧ *path*(v1) 
⇒ l by Proposition 1, and then ϕ ⇒ ¬*path*(v1) ∨ l, it is obvious that ¬*path*(v1) ∨ l is a non-tautology clause and xn does not appear in it, this is impossible. So there does not exist some node v2 such that var(v2) = xn, otherwise we have that: any father v3 of v2 satisfies L∞(v3) = ∅ by Definition 3 and Proposition 2; the children of v2 are ⊥ and 
〈∅〉 by Definition 4. These two assertions conflict with each other. Then given any True node v4, L∞(v4) has no other literal except xn and ¬xn for the same reason as v1. In summary, given any node v′ in ROBDD-1, | L∞(v1) | ≤ 1. 

Then by Definition 5, all of the ROBDD-i corresponding to ϕ are the same. 

We call Add-to-inf(u) to transform the ROBDD into the ROBDD-∞. Given any non-terminal node u1 in ROBDD with var(u1) < xn, neither of its children is the False node, otherwise, without loss of generality, assume that lo(u1) = ⊥, ϕ ∧ path(u1) ⇒ var(u1), and then ϕ ⇒ ¬path(u1) ∨ var(u1), it is obvious that ¬path(u1) ∨ var(u1) is a non-tautology clause and xn does not appear in it, this is impossible. So there exists some path from u1 to u2 such that var(u2) = xn, otherwise φ(u1) ⇔ *true*. Obviously, one child of u2 is ⊥, while other child is 〈∅〉. So xn cannot be omitted in any non-terminal node in ROBDD. Then the number of non-terminal nodes such that neither of its children is the False node in ROBDD is not more than | u | − 3. We have that | v | ≤ 2 ⋅ (| u | − 3) + 1 = 2 ⋅ | u | − 5 by Proposition 4. 

Let non-False node u3 be one child of u1, the new node created in the single call of Add-to-inf-sub(u1) must be equivalent to φ(u3) if L∞(u3) is empty, the new node must be equivalent to φ(u3) or φ(u3) | xn if xn ∈ L∞(u3), the new node must be equivalent to φ(u3) or φ(u3) | ¬xn otherwise. Let Φ1 = {φ(u3): L∞(u3) = ∅, u3 ≠ 〈∅〉}, Φ2 = {φ(u3): xn
∈ L∞(u3)}, Φ3 = {φ(u3) | xn: xn ∈ L∞(u3)}, Φ4 = {φ(u3): ¬xn ∈ L∞(u3)}, Φ5 = {φ(u3) | ¬xn: ¬xn ∈ L∞(u3)}. Obviously, the elements in Φj (1 ≤ j ≤ 5) are not equivalent to each other, the elements in Φ1 ∪ Φ2 ∪ Φ4 are not equivalent to each other, | Φ1 ∪ Φ2 ∪ Φ4 | = | Φ1 | + | Φ2 | + | Φ4 | = | u | − 3 (without the root u and the terminal nodes). Given any formula ϕ1 ∈ Φ1 ∪ Φ2 ∪ Φ3 ∪ Φ4 ∪ Φ5 without the appearance of xn, ϕ1 could only appears in Φ1, Φ3 and Φ5 if ϕ1 = *true*, otherwise ϕ1 could only be equivalent to some formula in Φ3 and Φ5 because xn cannot be omitted in any non-terminal node in ROBDD. Let Φ6 = {ϕ1: ϕ1 ∈ Φ3 and ϕ1 is equivalent to some formula in Φ5}. It is obvious that 6 35 24 | |3 | | min(| |,| |) min(| |,| |) 2
⎡ u − ⎤ Φ≤ Φ Φ = Φ Φ ≤ ⎢ ⎥ ⎢ ⎥
and each element in ROBDD corresponds to at least one node in the output of Add-to-inf-sub(u). By Observation 1, we only need to delete redundant nodes from the output of Add-to-inf-sub(u) because the input is an ROBDD, then we have that 

$v\geq1+(|u|-3)-|\Phi_{6}|\geq1+\left[\frac{|u|-3}{2}\right]=\left[\frac{|u|-1}{2}\right]$
u u v u ⎡ − ⎤⎡ ⎤ − ≥ + − −Φ ≥ + = ⎢ ⎥⎢ ⎥ ⎢ . ■
Now we turn to show that ROBDD-∞ is strictly less succinct than FBDD: 
Proposition 7. ROBDD-∞ is strictly less succinct than FBDD. Proof. First, we use a specific algorithm to show that FBDD is as succinct as ROBDD-∞. An algorithm which can transform any ROBDD-∞ into the equivalent FBDD in polytime is presented in Figure 7. Here we treat FBDD as a subset of BDD-0, i.e., for any non-False in FBDD, L(v) = ∅. By induction, it is easy to prove that Inf2FBDD is correct. 

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

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

Then we show that ROBDD-∞ is not as succinct as FBDD by given a counterexample. Let us consider the formula ϕ = (x1 ↔ y1) ∨ … ∨ (xn ↔ yn) over the variables order x1 < … < xn < y1 < … < yn. It is well known that 