Reduced ordered binary decision diagram with implied literals: a new knowledge compilation approach

摘要

Reduced ordered binary decision diagram (ROBDD) is one of the most influential knowledge compilation languages. We generalize it by associating some implied literals with each node to propose a new language called ROBDD with implied literals (ROBDD-\(L\)) and show that ROBDD-\(L\) can meet most of the querying requirements involved in the knowledge compilation map. Then, we discuss a kind of subsets of ROBDD-\(L\) called ROBDD-\(L_i\) with precisely \(i\) implied literals \((0\le i\le \infty )\), where ROBDD-\(L_0\) is isomorphic to ROBDD. ROBDD-\(L_i\) has uniqueness over any given linear order of variables. We mainly focus on ROBDD-\(L_\infty \) and demonstrate that: (a) it is a canonical representation on any given variable order; (b) it is the most succinct subset in ROBDD-\(L\) and thus also meets most of the querying requirements; (c) given any logical operation ROBDD supports in polytime, ROBDD-\(L_\infty \) can also support it in time polynomial in the sizes of the equivalent ROBDDs. Moreover, we propose an ROBDD-\(L_i\) compilation algorithm for any \(i\) and an ROBDD-\(L_\infty \) compilation algorithm, and then we implement an ROBDD-\(L\) package called BDDjLu. Our preliminary experimental results indicate that: (a) the compilation results of ROBDD-\(L_\infty \) are significantly smaller than those of ROBDD; (b) the standard d-DNNF compiler c2d and our ROBDD-\(L_\infty \) compiler do not dominate the other, yet ROBDD-\(L_\infty \) has canonicity and supports more querying requirements and relatively efficient logical operations; and (c) the method that first compiles knowledge base into ROBDD-\(L_\infty \) and then converts ROBDD-\(L_\infty \) into ROBDD provides an efficient ROBDD compiler.