The results in Table 3 show that the compilation quality of BDDjLu for ROBDD-∞ is higher than c2d for CBS_k3_n100_m403_*, par8-2-c, par15-2-c, uf200-01, uf200-02 and sat-grid-pbl-0015. And c2d is more high-quality for flat200-2, flat200-3 and uf200-03. c2d cannot compile hole10, while BDDjLu cannot compile flat200-1 and sat-grid-pbl-0020 6 . Neither c2d nor BDDjLu can compile par32-2-c and sat-grid-pbl-0025. 

Compared with the experimental results in [20], the FBDD generated by Inf2FBDD is obviously smaller for flat200-* and uf200-*. For all instances that can be compiled into ROBDD-∞, the size of ROBDD-∞ is obviously small than FBDD, while the size of FBDD is obviously smaller than ROBDD except sat-grid-pbl-0015. These validate the assertion in Section 3. Turning to running time, BDDjLu for ROBDD-∞ is faster than c2d except flat200-1 and sat-grid-pbl-*7. flat200-2, flat200-3 and uf200-* can be compiled by transforming the corresponding ROBDD-∞ into ROBDD now, while the ROBDD compiler reported in [20] cannot compile them in 900s with a 2.4 GHz CPU and 4 GB RAM. 

Overall, the ROBDD-∞ is obviously smaller than the ROBDD for each instance. The algorithm Build-inf in BDDjLu is more high-quality than c2d for the benchmark corresponding to small ROBDD-∞, and it is faster for most of problems when c2d uses min-fill heuristic to construct d-trees. Compared with the compilers reported in [20], it seems that Inf2FBDD and Inf2ROBDD are two good alternatives to compile CNF formulas into FBDDs and ROBDDs, respectively. As the time cost of employing SAT solver in Build-inf plays a very important role in the total running time of generating ROBDD-∞, we shall straight embed some highly efficient modern SAT solver into BDDjLu. In addition, we shall design good variables order rather than current simple order in BDDjLu to generate more space-efficient compilation results in future. 

Finally, we note that, in comparison with d-DNNF, FBDD and ROBDD, we need a little additional processing on the implied literals of ROBDD-∞ in the querying. Fortunately, on the one hand, some operations (e.g., model counting, computing the minimum cardinality) only need some fragment information about implied literals, therefore, we can visit any node of ROBDD-∞ in constant time; on the other hand, we can reduce the number of processing for other operations with the use of implied literals table. 

## 7 Conclusions

In this paper, we introduce a new compilation approach ROBDD-L by associating some implied literals in each node of ROBDD. Then an interesting kind of subsets of ROBDD-L is discussed: given a number i, we call the corresponding subset ROBDD-i, which requires that all of its nodes should be precisely associated by i implied literals. In particular, the ROBDD-0 whose nodes have no implied literal is isomorphic to ROBDD; the ROBDD-∞
requires that every node should be associated by the implied literals as many as possible. Given a number i and a Boolean formula, we show that there is exactly one ROBDD-i representing it over a specific variables order. 

Furthermore, we show that every sentence of OBDD-L can be transformed into an equivalent sentence of ROBDD-∞ in polytime. This means that ROBDD-∞ is the most succinct subset of OBDD-L. Particularly, ROBDD-∞ is strictly more succinct than ROBDD. Compared with FBDD and d-DNNF, ROBDD-∞ is strictly less succinct. And we propose the algorithm Inf2FBDD which can transform any ROBDD-∞ into FBDD. In order to evaluate the inferential power of this interesting subset, we compare it with ROBDD, FBDD and d-DNNF by the operations that can be supported in polytime with respect to the knowledge compilation map. For the queries, ROBDD satisfies SE which ROBDD-∞ does not satisfy, while ROBDD-∞ satisfies EQ which FBDD and d-DNNF does not satisfy. For the transformations, ROBDD satisfies CD, SFO, ∧BC, ∨BC and ¬C, both ROBDD-∞ and d-DNNF only satisfy CD, and FBDD satisfies CD and ¬C. 

Finally, we propose the compilation algorithm Build which can compile any Boolean formula into a ROBDD-i for any i. Based on it, we propose the ROBDD-∞ compilation algorithm Build-inf and discuss three optimization techniques. In addition, we show that every ROBDD-∞ can be transformed into ROBDD by proposing the algorithm Inf2ROBDD. Combining Build, Build-inf, Inf2FBDD, Inf2ROBDD and all the operations supported by ROBDD-L in polytime, we devise the ROBDD-L package BDDjLu and test it on some benchmarks from SATLIB. Preliminary experimental results show that: for the same instance, ROBDD-∞ is obviously smaller than ROBDD; Build-inf in BDDjLu is more high-quality than c2d for the benchmarks corresponding to small compilation results, and it is faster for most of problems when c2d uses min-fill heuristic to construct d-trees; it seems that it is better to transform the ROBDD-∞ into FBDD and ROBDD using Inf2FBDD and Inf2ROBDD. 

And both efficiency and compilation quality of BDDjLu have potential to be improved by embedding a modern SAT solver and devising a better variables order. 