procedure Build-inf(ϕ) 

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

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

3: C′ ← ∅
8: **endif** 9: **endwhile** 
10: **return** C′
15: ϕ ← ϕ | L(v) 
17: **else** 
22: **endif**
24: M ← Decide(ϕ) 
Obviously, by using Get-imps, we can significantly reduce the number of calling the function Decide. In fact, the efficiency of the algorithm is heavily dependent on the calling number and efficiency of Decide. So Get-imps is helpful for improving the efficiency. It is pointed out that we can limit the literals in C to the ones appearing in ϕ on Line 2 if ϕ is in NNF because a NNF formula can only imply the literals appearing it. By some proof analogous to the one of Proposition 10, the algorithm Build-inf is correct: 
Proposition 11. Given any propositional formula ϕ, Build-inf(ϕ) can terminate in finite time and its output is the corresponding ROBDD-∞. 

## 5.2 Some Techniques To Improve The Performance Of Build-Inf

The algorithm Build-inf in Figure 11 is adapted to any propositional formula. However, knowledge base often is represented as a CNF formula as human can read and write it with ease. Here are some techniques which are potential to improve the performance of Build and Build-inf to compile a CNF formula: (1) aims at reducing the number of calling the function Decide, (2) is used to reduce the time of such calling, and the purpose of (3) is to reduce the number of recursive calling of Build-inf-sub. 

(1) Horn lower approximation As previously pointed out, the efficiency of the algorithm is heavily dependent on the calling number of Decide. Given a CNF formula ϕ, a Horn lower approximation is a Horn theory implying ϕ, so ϕ implies a literal only if any Horn lower approximation of ϕ implies it. And it is well known that all implied literals of Horn theory can be computed in polytime. We exploit these properties to reduce the number of calling Decide, i.e., the function Get-imps will be displaced by the function Get-imps-CNF in Figure 12. We give an example to show how Get-imps-CNF works. 

Example 2. Let ϕ = {x1 ∨ x3, ¬x2 ∨ x3, ¬x1 ∨ ¬x4, x3 ∨ x4} and Ω = ∅. C = {x1, ¬x1, x2, ¬x2, x3, ¬x3, x4, ¬x4} 
after running Line 11. Obviously, ϕ does not imply x1. Assume that Decide(ϕ ∪ {¬x1}) on Line 14 returns a model M = {¬x1, ¬x2, x3, ¬x4}. Then Horn-app(ϕ, M) generates a Horn lower approximation ϕ′ = {x3, ¬x2 ∨ x3, ¬x1 ∨ ¬x4}. ϕ′ only implies x3. After running Line 17, C = {x3}. Then we find that ϕ also implies x3. Note that we only need to employ SAT solver twice here, while solver will be called at least 3 up to 5 times in Get-imps (dependent on the models obtained by solver). 

In fact, a model M of ϕ is also a Horn lower approximation (each literal in M can be seen as a unit Horn clause). However, the approximation generated by Horn-app(ϕ, M) is obviously greater than M, i.e., M ⇒
Horn-app(ϕ, M), for example, the Horn approximation in Example 2 have 6 models. The idea of Horn theory approximation in [1] is generating a greatest lower bound (GLB). However, [21] showed that this problem is at least NP[ (log )] p O n -hard. It seems that generating a GLB is not desirable in Build-inf. 