

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

Proposition 4. ROBDD-∞ is the most succinct subset in OBDD-L. In fact, given any OBDD-L, let n be the number of the non-terminal nodes such that neither of its children is the False node, then this OBDD-L can be transformed into the corresponding ROBDD-∞ in polytime and the nodes of the ROBDD-∞ is not more than 2n + 1. 

Proof. We use a specific algorithm to prove this proposition. An algorithm which can transform any OBDD-L
into the equivalent ROBDD-∞ in polytime is presented in Figure 5. In order to avoid making too many recursive calls, we maintain a cache G2 which stores previously computed outputs of the function Add-to-inf-sub. On Lines 5-9, we search the nearest node v′ from v such that neither of the children of v′ is the False node. It is obvious that this loop can terminal in polytime. 

We first show that the output of Add-to-inf-sub is indeed an OBDD-∞ equivalent to its input such that VARS(u) ⊆ *VARS*(v), and then Reduce(Add-to-inf-sub(v)) returns the corresponding ROBDD-∞ by Proposition 3. 

We prove it by induction on the size of | v |. The case | v | = 1 is immediate. Assume that the conclusion holds for | v | ≤ n. When | v | = n + 1, the output of Add-to-inf-sub obviously meets the requirements if v′ is a True node. 

Otherwise we have | lo(v′) | ≤ n and | hi(v′) | ≤ n. By the induction hypothesis, the output of Add-to-inf-sub(lo(v′)) 
(resp. Add-to-inf-sub(hi(v′)) is an OBDD-∞ equivalent to φ(lo(v′)) (resp. φ(hi(v′))). After Line 15 (resp. Line 17), 
the BDD-L with the root lo(u) (resp. hi(u)) is still an OBDD-∞. Given any literal l ∈ L(u) and x is the variable of l, if l appears in v′ or some ancestor node of v′, and then x doesn't appear in any descendent node of v′, we have that x doesn't appear in any descendent node of u because VARS(lo(u)) ⊆ *VARS*(lo(v′)) and VARS(hi(u)) ⊆ *VARS*(hi(v′)) 
by the induction hypothesis. Otherwise l ∈ L∞(lo(v′)) and l ∈ L∞(hi(v′)) by Definition 2, then by Proposition 1 and the induction hypothesis, l ∈ L(Add-to-inf-sub(lo(v′))) and l ∈ L(Add-to-inf-sub(hi(v′))), then l is deleted on Lines 15 and 17, it means that x doesn't appear in any descendent node u. So the output of Add-to-inf-sub(v) is a BDD-L. 

By Definition 3, var(v′) is less than any variable appearing in lo(v′) and hi(v′), and then var(v′) is less than any variable appearing in lo(u) and hi(u) because VARS(lo(u)) ⊆ *VARS*(lo(v′)) and VARS(hi(u)) ⊆ *VARS*(hi(v′)). We know that L(lo(u)) does not share any literal with L(hi(u)) and neither of lo(u) and hi(u) is the False node, this means that L(u) = L∞(u) by Definition 2, and then the condition 3 of Definition 3 is satisfied in v. So the output of Add-to-inf-sub(v) is an OBDD-∞. 

Then we show that the call of Add-to-inf-sub(v) can terminate in polytime for any ROBDD-L with the root v, then Add-to-inf(v) can terminate in polytime because we can compute L∞(v′) for any node v′ in polytime (Line 23) 
and the output can be transformed into the equivalent ROBDD-∞ in polytime by Proposition 3 on Line 24. It is obvious that a single call of Add-to-inf-sub can terminate in polytime because every step except the recursive calls can terminal in polytime. With the cache G2, there are at most n recursive calls of Add-to-inf-sub. So Add-to-inf-sub(v) can terminate in polytime. 

Finally, in a single call of Add-to-inf-sub, exactly two new nodes (i.e., lo(u) and hi(u)) will be introduced into the resulting OBDD-∞. Together with the root, there exist 2n + 1 nodes in the resulting OBDD-∞. By Proposition 3, there exist at most 2n + 1 nodes in the resulting ROBDD-∞. In summary, the conclusion holds. ■
It is pointed out that the algorithm Add-to-inf immediately give us a ROBDD-∞ compilation method, i.e., 
firstly compile the knowledge base into ROBDD, and then use the algorithm Add-to-inf to turn the result into ROBDD-∞. In addition, we point out one observation about Add-to-inf as follows: 