ROBDD-i with the root u must have two identical children by the induction hypothesis. This conflicts with the condition 1 of Definition 4. So the formula represented by low (resp. high) child of v1 must be equivalent to the one represented by low (resp. high) child of v2 (otherwise the formula represented by v1 is not equivalent to the one represented by v2), then we know that the low (resp. high) child of v1 is identical to the low (resp. high) child of v2 by induction hypothesis. This means that v1 is identical to v2. ■

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

Figure 3. An example about OBDD-i (left) and ROBDD-i Although any ROBDD-i is a reduced OBDD-i, there exists some OBDD-i (0 < i < ∞) such that the corresponding ROBDD-i has more nodes. An example is showed in Figure 3, where the OBDD-i has 5 nodes and the ROBDD-i has 7 nodes. However, this kind of "strange phenomenon" will not occur when i = 0 or i = ∞. 

Proposition 3. Given any formula ϕ, the corresponding ROBDD-i has the least number of nodes among all OBDDs-i equivalent to ϕ and each OBDD-i can be transformed into the equivalent ROBDD-i in linear time if i = 0 or i = ∞. 

Proof. An algorithm called Reduce which can transform any OBDD-i into the corresponding ROBDD-i in linear time is presented in Figure 4. The function MK is called to guarantee the condition 2 of Definition 4: given any node u, if some identical node has appeared before, then MK(v) returns the old one, otherwise it returns u. The condition 1 of Definition 4 is guaranteed by Line 5 (no matter whether i = ∞ or not, L(lo(u)) = ∅ if lo(u) = hi(u), so L(u) does not need to be changed). Every step in a single call (without consideration of the recursive calls) of Reduce can terminal in constant time, include the call of MK, whose running time is constant (readers are referred to [9] for the reason). With the cache G1, there are at most | v | recursive calls of Reduce. So Reduce(v) can terminate in linear time. And in a single call of Reduce, at most one new node is introduced into the result (i.e. a new node is introduced only when MK(u) returns u itself). We have that the nodes in the resulting ROBDD-0 or ROBDD-∞ is not more than the ones in the input. Then the conclusion is obvious by Proposition 2. ■

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

## 3 On The Succinctness Of Robdd-L

In this section, we first show that ROBDD-∞ is the most succinct part in OBDD-L, then prove that ROBDD-i is not at least as succinct as ROBDD-j for i < j. These mean that ROBDD-i is indeed a different target language from ROBDD-j with i ≠ j and ROBDD-∞ is strictly more succinct than any ROBDD-i (i < ∞), including ROBDD. 

Finally, we show that ROBDD-∞ is strictly less succinct than any FBDD. From these results, we can obtain some other conclusions. The definition of succinctness is as follows [5]: 
Definition 7. Let L1 and L2 be two subsets of NNF. L1 is at least as succinct as L2, if and only if there exists a polynomial p such that for every sentence α ∈ L2, there exists an equivalent sentence β ∈ L1 where | β | ≤ p ⋅ | α |. 

Here, | α | and | β | are the sizes of α and β, respectively. L1 is strictly more succinct than L2 if and only if L1 is at least as succinct as L2, while L2 is not at least as succinct as L1. 

Note that on the one hand the fact L1 is strictly less succinct than L2 does not prevent that L1 is more space efficient than L2 for some kind of knowledge bases, on the other hand the succinctness is only concerned about the best case, in fact for the compilation languages without uniqueness, the time cost of finding the best representation of the knowledge base is so high that usually it is impractical to use such kind of algorithms. Therefore, it is possible that given two languages L1 and L2 such that L1 is strictly more succinct than L2, compared with the L2 compilers, some L1 compiler can generate more space efficient compilation results for some kind of knowledge bases. We will validate this assertion in Section 6. 