# Reduced Ordered Binary Decision Diagram With Implied Literals: A New Knowledge Compilation Approach

## Yong Lai, Dayou Liu, **Shengsheng Wang** College Of Computer Science And Technology

Jilin University, Changchun 130012, P.R. China. 

e-mail: laiy07@mails.jlu.edu.cn Abstract: Knowledge compilation is an approach to tackle the computational intractability of general reasoning problems. According to this approach, knowledge bases are converted off-line into a target compilation language which is tractable for on-line querying. Reduced ordered binary decision diagram (ROBDD) is one of the most influential target languages. We generalize ROBDD by associating some implied literals in each node and the new language is called reduced ordered binary decision diagram with implied literals (ROBDD-L). Then we discuss a kind of subsets of ROBDD-L called ROBDD-i with precisely i implied literals (0 ≤ i ≤ ∞). In particular, ROBDD-0 is isomorphic to ROBDD; ROBDD-∞ requires that each node should be associated by the implied literals as many as possible. We show that ROBDD-i has uniqueness over some specific variables order, and ROBDD-∞ is the most succinct subset in ROBDD-L and can meet most of the querying requirements involved in the knowledge compilation map. Finally, we propose an ROBDD-i compilation algorithm for any i and a ROBDD-∞ compilation algorithm. Based on them, we implement a ROBDD-L package called BDDjLu and then get some conclusions from preliminary experimental results: ROBDD-∞ is obviously smaller than ROBDD for all benchmarks; ROBDD-∞ is smaller than the d-DNNF the benchmarks whose compilation results are relatively small; it seems that it is better to transform ROBDDs-∞ into FBDDs and ROBDDs rather than straight compile the benchmarks. Key words: knowledge compilation, target language, ROBDD, implied literals 

## 1 Introduction

Reasoning problems in their general form are intractable and knowledge compilation has been emerging as a key direction of research for dealing with such kind of intractability [1-5]. The basic idea of knowledge compilation is to split the reasoning process into two phases: an off-line compilation phase, in which the propositional theory is compiled into some tractable target language, and an on-line query-answering phase, in which the compiled target is used to efficiently answer the queries. And the compiling time in off-line phase can be amortized by a (potentially) exponential number of on-line queries. 

The target language is one of key aspects for any compilation approach. There have existed dozens of target languages so far, such as Horn theories [1], prime implicates/implicants [6, 7], reduced ordered binary decision diagram (ROBDD) [8, 9], free binary decision diagram (FBDD) [5, 10], decomposable negation normal form 
(DNNF, three subsets d-DNNF, DNNFT and d-DNNFT) [3, 11, 12], EPCCL theory [4, 13] and so on. Therefore, it is important to choose an appropriate target language in practical applications. Darwiche and Marquis argue that the choice of a target language must be based on two key aspects: the succinctness of the target compilation language, and the class of queries and transformations that the language supports in polytime [5]. Moreover, they propose the classic knowledge compilation map, which analyzes many existing target compilation languages according to the above aspects. On this basis, some researchers extend the knowledge compilation map [12, 14, 15]. 

ROBDD is one of the most tractable target languages which satisfy all of querying requirements involved in the knowledge compilation map (as far as we know, the compilation languages meeting these requirements include ROBDD, MODS, d-DNNFT and EPCCL theory [5, 12, 13]) and has been quite influential in many communities such as model checking [16], AI planning [17], abductive inference [18], terminological reasoning in description logic SHIQ [19] and so on. However, ROBDD seems a bit redundant for some Boolean formulas. For example, it is well known that the ROBDD representing the Boolean formula (x1 ↔ y1) ∧ … ∧ (xn ↔ yn) has exponential size over the variables order x1 < … < xn < y1 < … < yn. In fact, when xi is assigned some value (true or *false*), yi must have the same value. This characteristic limits the application of this language to some specific areas. Therefore, in order to reduce this kind of redundancy and extend its real applications, it is very necessary to make some small changes of ROBDD without loss of too much tractability. Based on this motivation, we do the following work in this paper: 
1. We add some literals called implied literals in the nodes of ROBDD meaning that the formula represented by the node implies them. We call this new target language ROBDD-L. Given a number i, we discuss a subset of ROBDD-L called ROBDD-i - precisely i implied literals in each node. It is obvious that ROBDD-0 is isomorphic to ROBDD. Then we show that there is exactly one ROBDD-i representing a given formula over a specific variables order. 

2. We show that ROBDD-∞ is an interesting subset of ROBDD-L: it is the most succinct subset of ROBDD-L
and we propose an algorithm which can transform every sentence of ROBDD-L into an equivalent sentence of ROBDD-∞ in polytime. Furthermore, we prove that ROBDD-∞ can meet all the query requirements except SE mentioned in the knowledge compilation map (it is unknown whether ROBDD-∞ satisfies SE or not). 

3. We propose a compilation algorithm (called Build) which can compile any Boolean formula into ROBDD-i
(0 ≤ i ≤ ∞). And we optimize Build to propose a ROBDD-∞ compilation algorithm called Build-inf and discuss three optimization techniques. In addition, we propose two algorithms called Inf2FBDD and Inf2ROBDD which 