Ordered Binary Decision Diagram With Implied Literals

Knowledge representation and reasoning is one of the most important sub-fields ofartificial intelligence. General reasoning problems are intractable from the viewpoint ofcomputational complexity. Knowledge compilation has emerged as a key direction of researchfor dealing with such kind of intractability. The target language is one of the key aspects forany compilation approach. So far, dozens of target languages have been proposed for differentinference tasks, and have been evaluated according their properties, including canonicity,succinctness and tractability. Among them, ordered binary decision diagram （OBDD） is acanonical and highly tractable language, and proved quite influential in a wide range ofpractical areas, including model checking, logic synthesis, diagnosis, product configuration,system design and automated planning.We generalize OBDD by associating some implied literals with each node to propose a newlanguage called OBDD with implied literals （OBDD-L）. By restricting the implied literals oneach node to be the first i （0≤i≤∞） literals （according to the linear order of variables） in allpotential implied literals, we get a subset of OBDD-L called OBDD-L_i. It is obvious thatOBDD-L0is isomorphic to OBDD. By imposing reducedness, we further get a subset ofOBDD-L_i called ROBDD-L_i. We show thatgiven any formula, there is exactly oneROBDD-L_iover a fixed variable order, where ROBDD-L0（resp. ROBDD-L_∞） have theminimum size among all equivalent ROBDD-L0’s （resp. ROBDD-L_∞’s）. We design analgorithm which can generate an ROBDD-L0（resp. ROBDD-L_∞） from an equivalentOBDD-L0（resp. OBDD-L_∞） in linear time.We propose an algorithm called L2Infty which can transform an OBDD-L into the equivalentROBDD-L_∞in O（n m）, where n is the number of nodes in OBDD-L and m is the number ofvariables in OBDD-L. Given i <j, we find a class of knowledge bases such that the sizes ofthe corresponding ROBDD-L_i’s are exponential butthe sizes of the correspondingROBDD-L_i+1’s are linear. Accordingly,ROBDD-L_iis not as less succinct as ROBDD-Lj;in particular, ROBDD-L_∞is not as less succinct as ROBDD-L_i. In addition, we comparethe succinctness relation between OBDD-L and some previous languages.We design the following algorithms which perform logical operations on OBDD-L or itssubsets: An algorithm which can check the consistency of OBDD-L in O（1）;An algorithm which can check the validity of OBDD-L in O（n）, and an algorithmwhich can check the validity of ROBDD-L_i（0≤i≤∞） in O（1）, where n is the numberof nodes in OBDD-L;An algorithm which can check whether an OBDD-L implies a clause in O（n₁n₂+n₃）, where n₁is the number of nodes in OBDD-L, n₂is the number of variables inOBDD-L, and n₃is the number of literals in the clause;An algorithm which can check whether a term implies an OBDD-L in O（n₁n₂+n₃）, where n₁is the number of nodes in the OBDD-L, n₂is the number of variables inOBDD-L, and n₃is the number of literals in the term;An algorithm which can count the models of OBDD-L in O（n）, where n is thenumber of nodes in OBDD-L;An algorithm which can enumerate the models of OBDD-L in O（n₁n₂n₃）, wheren₁, n₂and n₃are the numbers of nodes, variables and models in OBDD-L, respectively;An algorithm which can check the equivalence relation between two OBDD-L’s inO（n₁n₂+n₃n₄）, where n₁and n₂are the numbers of nodes and variables in anOBDD-L, respectively, and n₃and n₄are the numbers of nodes and variables in the otherOBDD-L, respectively;An algorithm which can condition an OBDD-L on a partial assignment in O（n₁n₂+n₃）, where n₁and n₂are the numbers of nodes and variables in the OBDD-L,respectively, and n₃is the number of variables in the assignment;An algorithm which can compute the minimum cardinality of OBDD-L in O（n）,where n is the number of nodes in OBDD-L;An algorithm which can minimize OBDD-L in O（n）, and another algorithm whichcan minimize ROBDD-L_∞in O（n m）, where n is the number of nodes in OBDD-L（resp. ROBDD-L_∞）, and m is the number of variables in the ROBDD-L_∞;Two algorithms which can forget OBDD-L and ROBDD-L_∞in O（n m2） on thelast variable, where n is the number of nodes in OBDD-L （resp. ROBDD-L_∞）, and m isthe number of variables in the OBDD-L （resp. ROBDD-L_∞）;Moreover, we prove the co-NP-completeness of deciding the entailment between twoOBDD-L’s （resp. ROBDD-L_∞’s）. According to the above analysis, we evaluate thetractability of OBDD-L and ROBDD-L_i（0≤i≤∞） up to the criterion in the knowledgecompilation map. We show that given any logical operation ROBDD-L0supports in polytime,ROBDD-L_∞can also support it in time polynomial in the sizes of the equivalent ROBDD-L0’s, and we propose a conjoining algorithm for ROBDD-L_∞, whose efficiency issometimes exponentially higher than the conjoining algorithm of ROBDD-L0.We propose an ROBDD-L_i（0≤i≤∞） compilation algorithm and an ROBDD-L_∞compilation algorithm, and then we implement an OBDD-L package called BDDjLu. Ourpreliminary experimental results indicate that:（a） the compilation results of ROBDD-L_∞aresignificantly smaller than those of ROBDD;（b） the standard d-DNNF compiler c2d and ourROBDD-L_∞compiler do not dominate the other, yet ROBDD-L_∞has canonicity andsupports more querying requirements and relatively efficient logical operations; and （c） themethod that first compiles knowledge base into ROBDD-L_∞and then converts ROBDD-L_∞into ROBDD outperforms other ROBDD compilers on most instances.