can transform any ROBDD-∞ into FBDD and ROBDD, respectively. Combining Build, Build-inf, Inf2FBDD and Inf2ROBDD and all the operations supported by ROBDD-L in polytime, we devise a ROBDD-L package called BDDjLu and report some experimental results. 

## 2 Reduced Ordered Binary Decision Diagram With Implied Literals

In the sequel X = {x1, … , xn} is the set of Boolean variables. A Boolean formula, hereafter simply called a formula, is constructed from true, *false* and variables using the negation operator ¬, conjunction operator ∧ and disjunction operator ∨. A *literal* is either a variable x (positive literal) or its negation¬x (negative literal). Given a literal l, its negation ¬l is ¬x if l is x and ¬l is x otherwise. A *clause C* is a set of literals representing their disjunction. C is a Horn clause if it contains at most one positive literal. A *term T* is a set of literals representing their conjunction. T is consistent iff there does not exist any variable x such that both x and ¬x belong to T. A 
Boolean formula in *conjunctive normal form* (CNF) is a set of clauses representing their conjunction. A CNF 
formula is Horn theory if all clauses are Horn clause. A Boolean formula in *negation normal form* (NNF) is constructed from true, *false* and literals using only the conjunction and disjunction operators. It is obvious that any clause, term and CNF formula is in NNF. A practical representation of NNF formula [3, 5] is a rooted, directed acyclic graph (DAG) where each leaf node is labeled with true, *false* or a literal; and each internal node is labeled with ∧ or ∨ and can have arbitrarily many children. 

An *assignment A* over the variables set X (we also say that A is a X-assignment) is a set of literals such that A
does not contains any literal and its negation. A is *complete* over X if A contains one and only one literal for any variable x in X (i.e., there exists exactly one element in {x, ¬x} ∩ A for any variable x ∈ X), otherwise it is *partial*. 

It is obvious that there exists 2| X | complete assignments over X. Any complete assignment satisfies *true* and falsifies *false*. A complete assignment A satisfies a literal l over X iff l ∈ A, A falsifies it otherwise; A satisfies a formula ¬ϕ over X iff it falsifies ϕ, and A falsifies it otherwise; A satisfies a formula ϕ1 ∧ ϕ2 over X iff it satisfies both ϕ1 and ϕ2, and A falsifies it otherwise; A satisfies ϕ1 ∨ ϕ2 over X iff it satisfies either ϕ1 or ϕ2, and A falsifies it otherwise. A *model M* of any formula is a complete assignment satisfies it. We call a formula *satisfiable* if it has at least one model, and we say it is *unsatisfiable* otherwise. We say a formula over X is a tautology if all complete assignments over X satisfy it. Given two formulas ϕ1 and ϕ2 over X, ϕ1 implies ϕ2 (denoted by ϕ1 ⇒ ϕ2) iff the models of ϕ1 is subsumed by the ones of ϕ2, ϕ1 is equivalent to ϕ2 (denoted by ϕ1 ⇔ ϕ2) iff both ϕ1 ⇒ ϕ2 and ϕ2 ⇒ ϕ1. Now we give the definition of *reduced ordered binary decision diagram with implied literals* step by step. 

Definition 1. A *binary decision diagram with implied literals* (BDD-L) is a rooted DAG. Each node v is either terminal or *non-terminal* and represents some formula φ(v) in NNF. There exist two kinds of terminal nodes: False node (denoted by ⊥) which represents *false*, and *True* nodes labeled by a set of literals L(v) called *implied* literals which represent the term conjoining all the literals in L(v). And each non-terminal node v is associated with a Boolean variable var(v), implied literals L(v) and two children, called low child lo(v) and *high* child hi(v). Given a non-False node v, it is denoted by 〈L(v)〉 if it is a True node, otherwise it is denoted by 〈var(v), lo(v), hi(v), L(v)〉. 

At each non-terminal node v, var(v) does not appear in L(v), any variable appearing in L(v) does not appear in its descendent nodes, and the low (resp. high) branch is depicted as a dash (resp. solid) line corresponding to the case where the variable is assigned *false* (resp. *true*). So given a non-terminal node v, we have that: 
φ( ) ( ( )) (( ( ) ( ( ))) ( ( ) ( ( )))). *v l L v var v lo v var v hi v* = ∈ ∧¬ ∧ ∨ ∧ ∧ φ φ ( ) ∗
Usually, an implied literal corresponds to a simple fact implied by knowledge base, such as John does not like pink coat, Jim just like jeans and so on. In BDD-L, some or all simple facts are pulled out and stored explicitly at the root. From above Definition 1, we know that the only difference between BDD-L and BDD [8] is the implied literals. When every node in BDD-L is mandatory for no implied literal, then BDD-L is equivalent to BDD and (*) 
will be φ(v) = (¬var(v) ∧ φ(lo(v))) ∨ (var(v) ∧ φ(hi(v))). And FBDD can be seen as a special kind of BDD-0 such that each variable appears at most once on any path. For simplicity, we suppose that at least one child of a non-terminate node is non-False and the implied literals of a non-False node represent a consistent tern. 

In the implementation, we use a hash table called nodes table to record all the nodes in BDD-L, another hash table called implied literals table, which allows us to deal with the same sets of implied literals only once in some operations (see Section 4), is used to record all the sets of implied literals in BDD-L, L(v) for any node v in the nodes table is an index pointing to some entry in implied literals table, L(u) and L(v) share the same entry if L(u) = L(v), the data unit size in implied literals table records the size of L(v) in order to facilitate model counting (see Section 4). 