
| Nodes Table   |       |     |      |    |
|---------------|-------|-----|------|----|
| ID            | var   | low | high | L  |
| 5             | x1    | 3   | 4    | 0  |
| 4             | x2    | 1   | 2    | 2  |
| 3             | x1    | 0   | 1    | 1  |
| 2             | True  | -   | -    | 1  |
| 1             | True  | -   | -    | 0  |
| 0             | False | -   | -    | -  |

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

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

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

Figure 1. An example about BDD-L
An example about BDD-L is showed in Figure 1. In the following, we denote the set of the variables appearing in v (i.e., var(v) and the variables appearing in L(v)) and its descendent nodes as *VARS*(v), the number of nodes in the BDD-L as | u |, where u is the root of the BDD-L, *path*(v) is a term and any literal ¬x (resp. x) belongs to it iff there exists some node v′ with the variable x such that its low (resp. high) branch appearing in the path from the root to v. The *maximal set of implied literals*, which is used frequently in this paper, is defined as follows: 
Definition 2. Given a BDD-L and a non-False node v in it, the maximal set of implied literals L∞(v) is defined as follows: 

$$L_{\infty}(v)=\begin{cases}L(v)&v\text{is a True node;}\\ L(v)\cup\{\text{\it var}(v)\}\cup L_{\infty}(hi(v))&lo(v)=\perp;\\ L(v)\cup\{\neg\text{\it var}(v)\}\cup L_{\infty}(lo(v))&hi(v)=\perp;\\ L(v)\cup(L_{\infty}(hi(v))\cap L_{\infty}(lo(v)))&\text{otherwise.}\end{cases}$$

Obviously, L(v) is a subset of L∞(v) for any non-False node v. Given any BDD-L, we can compute the maximal set of implied literals for all of its nodes in polytime with the use of dynamic programming, which is used in almost all algorithms in this paper. 

Definition 3. A BDD-L is *ordered* (OBDD-L) if 1. The set of variables is imposed over a given linear order <; 
2. Given a node u and its child v, var(u) is less than any variable appearing in v; 3. For any non-terminal node v, any variable appearing in L(v) is less than the ones appearing in L∞(v) but not in L(v), formally, x((( ( ) ( )) ( ( ) \ ( ) ( ) \ ( ))) ). *x Lv x Lv x L v Lv x L v Lv x x* ∞ ∞ ∀ ∈ ∨¬ ∈ ∧ ∈ ∨¬ ∈ → < ′ ′ ′
From the above definition, it is obvious that BDD-L in Figure 1 is not ordered as it does not satisfy the condition 2 and 3 in Definition 3, and we have some simple conclusions which are used in the proofs of some propositions: given a non-False node v, it is easy to prove that φ(v) is satisfiable (used in the proof of Proposition 1) 
by induction, because at least one child of v is non-False and the implied literals represent a consistent term; given any node u and its child v in an OBDD-L, VARS(v) ⊂ *VARS*(u) (used in the proof of Proposition 4); given a non-False node v, the condition 3 is obviously satisfied if L(u) = L∞(u) (used in the proof of Proposition 4). And the following proposition holds: 
Proposition 1. Given any non-False node v in any OBDD-L, each element in L∞(v) is exactly a literal implied by φ(v), i.e., L∞(v) = {l : φ(v) ⇒ l}. 

Proof. By induction on the size of | v |. Assume that the conclusion holds for | v | ≤ n. The case | v | = 1 is immediately. We proceed by case analysis: 
(1) lo(v) = ⊥: We have that L∞(v) = L(v) ∪ {var(v)} ∪ L∞(hi(v)) from Definition 2. By induction hypothesis, L∞(hi(v)) = {l : φ(hi(v)) ⇒ l}. This means that there exists some formula ϕ such that φ(hi(v)) ⇔ ∧(l ∈ L∞(hi(v))) ∧
ϕ. Then by (*) 
φ( ) ( ( )) ( ( ) ( ( ( ))) ). *v l L v var v l L hi v* =∈ ∧ ∧∈ ∧ ∧ ∧ ∞ ϕ It is obvious that φ(v) ⇒ l for any l ∈ L∞(v). Assume that there exists some literal l such that φ(v) ⇒ l and l ∉ L∞(v). 

And any non-False node in OBDD-L represents a satisfiable formula. Then ϕ ⇒ l, this conflicts with the induction hypothesis. 

(2) hi(v) = ⊥: It is analogous to (1). 

(3) Otherwise, we have that L∞(v) = L(v) ∪ (L∞(lo(v)) ∩ L∞(hi(v))) from Definition 2. By induction hypothesis, L∞(hi(v)) = {l : φ(hi(v)) ⇒ l} (resp. L∞(lo(v)) = {l : φ(lo(v)) ⇒ l}). This means that there exists some formula ϕ such that φ(hi(v)) ⇔ ∧(l ∈ L∞(hi(v))) ∧ ϕ (resp. φ(lo(v)) ⇔ ∧(l ∈ L∞(lo(v))) ∧ ϕ′). Then by (*) 
φ( ) ( ( )) (( ( ) ( ( ( ))) ) ( ( ) ( ( ( ))) )). *v l L v var v l L lo v var v l L hi v* = ∈ ∧¬ ∧ ∈ ∧ ∨ ∧ ∈ ∧ ∧∧ ∧ ∞ ∞ ϕ ϕ′
It is obvious that φ(v) ⇒ l for any l ∈ L∞(v). Assume that there exists some literal l such that φ(v) ⇒ l and l ∉ L∞(v). 

By Definition 3, then ϕ ⇒ l or ϕ′ ⇒ l, this conflicts with the induction hypothesis. ■
If we displace the OBDD-L with BDD-L in Proposition 1, then the proposition doesn't hold. The BDD-L in Figure 1 is a counterexample for it, where L∞(v) = ∅ and the formula represented by this BDD-L implies any 