there exists a linear FBDD equivalent to ϕ and the size of ROBDD representing ϕ is exponential. Obviously, ϕ does not imply any non-tautology clause without the appearance of yn. By Proposition 6, the size of ROBDD-∞
representing ϕ is exponential. So the conclusion holds. ■
By Propositions 4, 5, 7, Proposition 3.1 in [5], and the transitivity of succinctness, we know that: 
Corollary 1. ROBDD-∞ is strictly less succinct than DNNF and d-DNNF; ROBDD-∞ is incomparable to DNF, CNF, IP and PI. 

## 4 The Operations Of Robdd-∞

We have showed that ROBDD-∞ is the most succinct subset in OBDD-L in the previous section. In order to evaluate the inferential power of this interesting subset, we analyze the operations that ROBDD-∞ supports in polytime with respect to the criterion proposed in the knowledge map in this section. The following queries and transformations have been considered in the knowledge map. We just recall them here and readers are referred to [5] for their importance. 

Definition 8. Given any subset L of NNF, 
L satisfies CO (resp. VA) iff there exists a polytime algorithm that maps every formula ϕ from L to 1 if ϕ is consistent (resp. valid), and to 0 otherwise; L satisfies CE iff there exists a polytime algorithm that maps every formula ϕ from L and every clause C to 1 if ϕ ⇒ C holds, and to 0 otherwise; L satisfies IM iff there exists a polytime algorithm that maps every formula ϕ from L and every term T to 1 if T ⇒ ϕ holds, and to 0 otherwise; L satisfies EQ (resp. SE) iff there exists a polytime algorithm that maps every pair of formulas ϕ, γ from L to 1 if ϕ ⇔ γ (resp. ϕ ⇒ γ) holds, and to 0 otherwise; L satisfies CT iff there exists a polytime algorithm that maps every formula ϕ from L and some the variables set X which includes all of the variables appearing in ϕ to a non-negative integer that represents the number of models of ϕ over X (in binary notation). 

L satisfies ME iff there exists a polynomial p(., .) and an algorithm that outputs all models of an arbitrary formula ϕ from L over some the variables set X which includes all of the variables appearing in ϕ in time p(n, m), where n is the size of ϕ and m is the number of its models over X. 

Definition 9. Given any subset L of NNF, 
L satisfies CD iff there exists a polytime algorithm that maps every formula ϕ from L and every consistent term T to a formula from L that is logically equivalent to ϕ | T. 

L satisfies FO iff there exists a polytime algorithm that maps every formula ϕ from L and every subset X of the set of variables appearing in ϕ to a formula from L that is equivalent to ∃X.ϕ, i.e. the formula that does not mention any variable from X and for every formula γ that does not mention any variable from X, we have ϕ ⇒ γ precisely when ∃X.ϕ ⇒ γ. If the property holds for singleton X, we say that L satisfies SFO. 

L satisfies ∧C (resp. ∨C) iff there exists a polytime algorithm that maps every finite set of formulas ϕ1, … , 
ϕn from L to a formula of L that is logically equivalent to ϕ1 ∧ … ∧ ϕn (resp. ϕ1 ∨ … ∨ ϕn). 

L satisfies ∧BC (resp. ∨BC) iff there exists a polytime algorithm that maps every pair of formulas ϕ and γ from L to a formula of L that is logically equivalent to ϕ ∧ γ (resp. ϕ ∨ γ). 

L satisfies ¬C iff there exists a polytime algorithm that maps every formula ϕ from L to a formula of L that is logically equivalent to ¬ϕ. 

| L       | CO   | VA   | CE   | IM   | EQ   | SE   | CT   | ME   |
|---------|------|------|------|------|------|------|------|------|
| ROBDD   | √    | √    | √    | √    | √    | √    | √    | √    |
| ROBDD-∞ | √    | √    | √    | √    | √    | ?    | √    | √    |
| FBDD    | √    | √    | √    | √    | ?    | o    | √    | √    |
| d-DNNF  | √    | √    | √    | √    | ?    | o    | √    | √    |

Table 1. The polytime query of ROBDD-∞. √ means "satisfies", means 
"does not satisfy unless P = NP", and ? means "unknown". 

o Table 1 summarizes query-related properties of ROBDD-∞. As ROBDD, FBDD and d-DNNF are three of the most widely used target languages in practical applications, their properties are also showed here for comparison. 

Proposition 8. The results in Table 1 hold. 

Proof. CO, VA and EQ: Recall that for any formula, there is exactly one ROBDD-∞ representing it. This means, in particular, that there is exactly one ROBDD-∞ for the constant formula *true* (resp. *false*): the True node with no implied literal (resp. False node). And given two ROBDDs-∞, they are equivalent if and only if they are the same. So we have that: (1) Deciding the satisfiability and validity of a ROBDD-∞ can be done in constant time, it means that CO and VA are satisfied; (2) Deciding the equivalence between two ROBDDs-∞ can be done in polytime, it means that EQ is satisfied. 

CT, CE, IM and ME: Counting the models of a ROBDD-∞ over a set of variables can be done in linear time. 

An algorithm is presented in Figure 8. A single call of Count can terminal in constant time with the data unit size in implied literals table. With the cache G4, the number of recursive calls is | v |. Then this algorithm has a linear time complexity. Furthermore, we prove that the result of Count(v, X) equals to the number of models of φ(v) over X by induction on the size of | v |. The case | v | = 1 is immediate. Assume that Count(v, X) returns the correct 