some specific models of propositional theory and devise another algorithm called Build-inf for ROBDD-∞. Finally, we introduce some techniques which are potential to improve the performance of Build and Build-inf when the input is in CNF. 

## 5.1 Compilation Algorithm

The compilation algorithm Build is presented in Figure 10. Its correctness is guaranteed by the following proposition. 

Proposition 10. Given any propositional formula ϕ, Build(ϕ, i) can terminate in finite time and its output is the corresponding ROBDD-i. 

Proof. Let X be the set of variables appearing in ϕ. We prove the proposition by induction on the size of | X |. 

Assume that Build(ϕ, i) can terminate in finite time and its output is the ROBDD-i corresponding to ϕ with the root v such that *VARS*(v) ⊆ X if | X | ≤ n. The case | X | = 0 is immediate. When | X | = n + 1, we proceed by case analysis: 
ϕ is unsatisfiable: The conclusion is obvious. 

ϕ is equivalent to *true* after Line 9: The conclusion is obvious. 

Otherwise: After Line 9, let X1 and X2 be the set of variables appearing in ϕ | ¬xj and ϕ | xj, respectively. By the induction hypothesis, Build(ϕ | ¬xj, i) (resp. Build(ϕ | xj, i)) can terminate in finite time and its output is the ROBDD-i corresponding to ϕ | ¬xj (resp. ϕ | xj) such that *VARS*(lo(v)) ⊆ X1 (resp. *VARS*(hi(v)) ⊆ X2). Then Build(ϕj, i) can terminate in finite time, *VARS*(v) ⊆ X, the conditions in Definition 1 and Definition 3 are satisfied. Lines 4-8 guarantee the condition in Definition 5. The loop on Lines 10-16 guarantees that ϕ | ¬xj is not equivalent to ϕ | xj. By Proposition 2, lo(v) is not identical to hi(v). The call of MK guarantees the condition 1 in Definition 4. 

And the loop must terminate at some j, otherwise the condition on Line 17 will be satisfied, which corresponds to the case that ϕ is equivalent to *true* after Line 9. Then the output of Build(ϕ, X, i) is the ROBDD-i corresponding to ϕ. ■

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

It is pointed out that Line 11 in the algorithm Build is not needed any more if i = 0 or ∞, and we just need to call the algorithm Reduce to turn the result into ROBDD or ROBDD-∞. Particularly, we do not even need to Line 1 and Lines 4-9 if i = 0, then Build is equivalent to Algorithm 5 in [20] when the input is in CNF. We can displace the algorithm Build with the algorithm Build-inf in Figure 11 if i = ∞. In the algorithm Build-inf, Decide(ϕ) will return a model of ϕ if it is satisfiable, otherwise the empty set will be returned. It is trivial to prove that it is correct to use the function Get-imps to compute all literals implied by ϕ. 