# knowledge_compilation_meets_logical_separability__ca57ea03.pdf

Knowledge Compilation Meets Logical Separability

Junming Qiu1, 2, Wenqing Li1, 2, Zhanhao Xiao3, Quanlong Guan1, 2*, Liangda Fang1, 4, 5*, Zhao-Rong Lai1, 2, Qian Dong1

1 Jinan University, Guangzhou 510632, China 2 Guangdong Institute of Smart Education, Guangzhou 510632, China 3 Sun Yat-sen University, Guangzhou 510006, China 4 Pazhou Lab, Guangzhou 510330, China 5 Guangxi Key Laboratory of Trusted Software, Guilin University of Electronic Technology, Guilin 541004, China {2040697476jnu, eskii0706}@stu2020.jnu.edu.cn; xiaozhh9@mail.sysu.edu.cn; {gql, fangld, laizhr, dongq8}@jnu.edu.cn

Knowledge compilation is an alternative solution to address demanding reasoning tasks with high complexity via converting knowledge bases into a suitable target language. Interestingly, the notion of logical separability, proposed by Levesque, offers a general explanation for the tractability of clausal entailment for two remarkable languages: decomposable negation normal form and prime implicates. It is interesting to explore what role logical separability on earth plays in problem tractability. In this paper, we apply the notion of logical separability in three reasoning problems within the context of propositional logic: satisfiability check (CO), clausal entailment check (CE) and model counting (CT), contributing to three corresponding polytime procedures. We provide three logical separability based properties: CO-logical separability, CE-logical separability and CT-logical separability. We then identify three novel normal forms: CO-LSNNF, CE-LSNNF and CT-LSNNF based on the above properties. Besides, we show that every normal form is the necessary and sufficient condition under which the corresponding procedure is correct. We finally integrate the above four normal forms into the knowledge compilation map.

Introduction Knowledge compilation (KC) has been attracted interests in many areas of AI, for example, model-based diagnosis (Huang and Darwiche 2005; Mateescu, Dechter, and Marinescu 2008), explainable machine learning (Shih, Darwiche, and Choi 2019; Darwiche and Hirth 2020), probabilistic inference (Martires, Dries, and De Raedt 2019; Shih, Choi, and Darwiche 2019) and planning (Palacios et al. 2005; Huang 2006) and so on. As an alternative solution to address demanding reasoning tasks with high complexity, KC converts knowledge bases into a target language in which such reasoning tasks can be tractably accomplished. Darwiche and Marquis (2002) proposed two criteria to evaluate target compilation languages: succinctness (the size of complied knowledge bases) and tractability (the supported polytime queries and transformations). In general, more succinct languages are less tractable and vice versa.

*Both are corresponding authors. Copyright 2022, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

One of primary purposes of KC is to design a suitable target language that achieves a good trade-off between succinctness and tractability for one or more specific reasoning tasks. In the past decades, many prominent target compilation languages were developed, particularly, decomposable negation normal form (DNNF), the subset of negation normal form (NNF) satisfying the -decomposability property (Darwiche 2001a). The author also designed two polytime procedures for satisfiability check and clausal entailment check, which are correct for DNNF. In other words, DNNF supports polytime satisfiability check and clausal entailment check. One question worth investigation is the intrinsic reason why DNNF supports such polytime queries. It actually can be answered by the notion of logical separability which was first proposed by Levesque (1998). Roughly speaking, a conjunction φ is logically separable, if the clausal entailment problem of a conjunction φ can be decomposed to entailment problems for every conjunct of φ. It is easily verified that any conjunction appearing in a DNNF-formula is logically separable due to the -decomposability property. In addition, prime implicate normal form (PI) supports polytime clausal entailment check as the conjunction of prime implicates is logically separable. Hence, logical separability offers a thorough explanation for why both DNNF and PI supports clausal entailment check. It is interesting to explore what role logical separability on earth plays in problem tractability. In the paper (Levesque 1998), Levesque also defined a normal form, namely Levesque s normal form (LNF), s.t. the entailment check is tractable for a class of knowledge bases. However, after that, the idea of logical separability has hardly been applied to language design for other reasoning problems. It motivates us to take logical separability into account to design succinct target languages in which reasoning problems are tractably solved. In this paper, we focus on three reasoning problems in the context of propositional logic: satisfiability check, clausal entailment check and model counting. For these three reasoning problems, we start by providing three polytime procedures CO, CE and CT , and then give definitions of logical separability based properties: CO-logical separability, CE-logical separability and CT-logical separability,

The Thirty-Sixth AAAI Conference on Artificial Intelligence (AAAI-22)

respectively. We also propose three novel normal forms: CO-LSNNF, CE-LSNNF and CT-LSNNF, each of which satisfies the above logical separability based properties, respectively, and show that every normal form is the necessary and sufficient condition under which the corresponding procedure is correct. In addition, CO-LSNNF, CE-LSNNF and CT-LSNNF are complete languages.

For CO-LSNNF, we provide two interesting theoretical results: (1) any language supports polytime satisfiability check iff it is polynomially translatable into CO-LSNNF; and (2) CO-LSNNF is equally succinct to NNF. For CE-LSNNF, we show that if a language is polynomially translatable into CE-LSNNF, then it supports polytime clausal entailment check; and make a comparison to LNF which is a strictly less succinct than CE-LSNNF. For CT-LSNNF, we prove that (1) if a language is polynomially translatable into CT-LSNNF, then it supports polytime model counting, and (2) CT-LSNNF is polynomially equivalent to d-DNNF.

Furthermore, we analyze the computational complexity of the membership problems of the three logical separabilitybased normal forms. Finally, we analyze the relative succinctness of CO-LSNNF, CE-LSNNF, CT-LSNNF and LNNF compared to the languages considered in (Darwiche and Marquis 2002; Fargier and Marquis 2014) and investigate which of the queries and transformations can be accomplished in polytime for them.

Preliminaries

The NNF Languages

Throughout this paper, we fix a finite set X of variables. A literal is a variable (positive literal) or a negated one (negative literal). For a positive (resp. negative) literal x (resp. x), its complementary literal is x (resp. x). Let Y X. A Y-literal is a literal x or x where x Y. A term (resp. clause) is , , or a conjunction (resp. disjunction) of literals. We say a term (resp. clause) is non-trivial if every variable appears at most once. Throughout this paper, we consider a wide range of complete propositional languages, all of which are the subsets of negation normal form (NNF). A NNF-formula is a rooted, directed acyclic graph (DAG), of which each leaf node is labeled by , , or literals; and each internal node is labeled by (conjunction) or (disjunction). We use a lower-case Greek letter (e.g. α, β) to denote a propositional formula. We use Var(α) (resp. Lit(α)) to denote the set of variables (resp. literals) appearing in α. We use |α| to denote the size of α (i.e. the number of its DAG edges). A Y-interpretation ω is a set of Y-literals s.t. each variable of Y appears exactly once. Let Var(α) Y. We use ω |= α to denote ω satisfies α, which is defined as usual. A Y-model of α is a Y-interpretation satisfying α. We use Mod Y(α) to denote the set of Y-models of α. For simplicity, in the case Y = X, we omit the subscript X, and Mod(α) denotes the set of X-models of α. We say α is satisfiable, if Mod(α) = ; otherwise, it is unsatisfiable.

As mentioned in (Darwiche and Marquis 2002), a language qualifies as a target language if it supports polytime clausal entailment check. NNF is not a desired target language as it does not support such a query unless P = NP. But many of its subsets, with one or more restrictions, do. Conjunctive normal form (CNF) is the conjunction of nontrivial clauses while its dual, disjunctive normal form (DNF), is the disjunction of non-trivial terms. A prime implicate c of α is an implicate of α and there is no implicate c = c s.t. α |= c and c |= c. Prime implicates (PI) is the subset of CNF where each formula α is a conjunction of all of the prime implicates of α. Its dual, prime implicants (IP), can be similarly defined. Decomposable NNF (DNNF) (Darwiche 2001a) is the subset of NNF satisfying -decomposability, requiring the sets of variables of the children of each -node in a formula to be pairwise disjoint. Deterministic DNNF (d-DNNF) (Darwiche 2001b) is the subset of DNNF satisfying determinism, requiring the children of each -node in a formula to be pairwise logically contradictory. KROM (Krom 1970) is the subset of CNF in which each clause contains at most two literals. HORN (Horn 1951) is the subset of CNF in which each clause contains at most a positive literal. K/H is the union of KROM and HORN. Renamable Horn (ren H) is the subset of all CNF-formulas α for which there is a subset Y of Var(α) s.t. the formula obtained by substituting in α every Y-literal l by its complement l is a HORN-formula. Fargier and Marquis (2014) applied disjunctive closure principle to KROM, HORN, K/H and ren H and obtained KROM[ ], HORN[ ], K/H[ ] and ren H[ ], respectively. We remark that the above normal forms are not only defined in purely syntactic style but also based on semantics. For example, CNF and DNF are syntactic normal forms. On the other hand, PI and d-DNNF are based on clausal entailment and satisfiability, respectively and hence being semantic normal forms.

Succinctness and Polynomial Translations We now consider two notions of translations on two subsets of NNF: succinctness and polynomial-translation. Definition 1. Let L1 and L2 be subsets of NNF. We say L1 is at least as succinct as L2, denoted L1 s L2, if there is a polynomial p s.t. for every formula α L2, there is an equivalent formula β L1 s.t. |β| p(|α|). L2 is polynomially translatable into L1, denoted L1 p L2, if there exists a (deterministic) polynomial-time algorithm f s.t. for every formula α L2, we have an equivalent formula f(α) L1. Succinctness only considers polynomial-space translations, that is, the size of the L1-formula β equivalent to α is required to be polynomial in the size of L2-formula α. Polynomial-translation is a more strict relation than succinctness, requiring polynomial-time translations, that is, any L2-formula can be tractably transformed into an equivalent L1-formula. Furthermore, we have L1 p L2 implies that L1 s L2 (Fargier and Marquis 2014). The two relations s and p are clearly reflexive and transitive, i.e. pre-orders over subsets of NNF. The notation

s denotes the symmetric part of s, that is, L1 s L2 iff L1 s L2 and L2 s L1. On the other hand, <s denotes the asymmetric part of s, that is, L1 <s L2 iff L1 s L2 and L2 s L1. In the following, L1 s L2 means that L1 s L2 unless the polynomial hierarchy PH collapses. The notations p, <p and p can be similarly defined.

Queries and Transformations

As pointed out in (Darwiche and Marquis 2002), another two crucial criteria for evaluating normal forms is the set of query and transformation tasks supported in polytime. To differentiate query (or transformation) tasks and properties, we use letters in typewriter type font for the former, and letters in the boldface font for the latter. A query task for a language L takes as input one or more L-formulas and possibly clauses and terms, and outputs a Boolean value, a natural number, or a set of interpretations. We consider the following query tasks:

Satisfiability (CO): check if α .

Validity (VA): check if α .

Casual entailment (CE): check if α|=c where c is a clause.

Term implication (IM): check if t |= α where t is a term.

Sentential entailment (SE): check if α |= β.

Equivalence (EQ): check if α β.

Model counting (CT): compute the size of Mod(α).

Model enumeration (ME): list every member of Mod(α).

A transformation task for L takes as input one or a set of L-formulas, possibly a term and a set of variables, and returns an appropriate L-formula. We consider the following transformation tasks:

Conditioning (CD): generate α|t where t is a satisfiable term;

Forgetting (FO): generate Y.α where Y X.

Singleton forgetting (SFO): generate {x}.α where x X.

Conjunction ( C): generate α1 αn.

Disjunction ( C): generate α1 αn.

Bounded conjunction ( BC): generate α β.

Bounded disjunction ( BC): generate α β.

Negation ( C): generate α.

Specifically, conditioning a formula α on a satisfiable term t, denoted by α|t, is the result of replacing each occurrence of a variable x in α by (resp. ), if x (resp. x) is a positive (resp. negative) literal of t. Forgetting Y from α, denoted as Y.α, is the strongest consequence that does not contains any variables of Y, that is, for any NNF-formula β s.t. Var(β) Y = , α |= β iff Y.α |= β. We say a language L satisfies the query (resp. transformation) property Q (resp. T), iff there is a polytime procedure for the query (resp. transformation) task Q (resp. T) for L. For example, DNF supports CO since the CO task can be performed under DNF in polytime (Darwiche and Marquis 2002).

Satisfiability We first present a procedure for satisfiability check on NNFformulas, which was proposed by Darwiche (2001a). Definition 2. The procedure CO(α) is recursively defined as: CO( ) = 1, CO( ) = 0 and CO(l) = 1 CO(β1 βn) = min 1 i n{CO(βi)}

CO(β1 βn) = max 1 i n{CO(βi)}

The above procedure works in a recursive way. In the base case, the Boolean constant and a literal l are satisfiable while is unsatisfiable. In the induction case, the satisfiability problem of an -node (or -node) is reduced to the same problem of its subformula βi. If some βi of -node α is satisfiable, then α is satisfiable. Similarly, if every βi of -node α is satisfiable, then α is satisfiable. Definition 3. Let L be a language, and f a procedure that takes an NNF-formula α as input, and that returns a Boolean value. We say f is CO-sound for L iff for every L-formula α, f(α) = 1 only if CO(α) = 1; f is CO-complete for L iff for every L-formula α, CO(α) = 1 only if f(α) = 1. The procedure CO is a CO-complete algorithm for any NNF-formula α and it can be evaluated in linear time in |α|. Theorem 1. (Darwiche 2001a) The procedure CO is COcomplete for NNF with the time complexity O(|α|). However, the procedure CO is unsound for NNF-formula. Let us consider the unsatisfiable formula α = x x. Clearly, CO(x) = CO( x) = 1. It follows that CO(α) = 1 which contradicts the unsatisfiability of α. The reason why the procedure CO cannot serve as a sound algorithm is that CO is a simple evaluation-based algorithm and it does not consider implicit logical contraditions occurring in some -nodes of an NNF-formula. Formally, we say an -node α = β1 βn contains an implicit logical contradiction, if α is unsatisfiable and each βi is satisfiable for 1 i n. In this case, CO(α) = 1 as CO(βi) = 1 for 1 i n, and hence deriving an incorrect result. We hereafter provide a necessary and sufficient condition on NNF for which the CO procedure is complete and sound. Definition 4. An NNF-formula α is CO-logically separable (COls) iff α is , , or a literal l; or α is an -node β1 βn, and if α is unsatisfiable, then βi is unsatisfiable and COls for some 1 i n; or α is an -node β1 βn, and if α is unsatisfiable, then βi is unsatisfiable and COls for every 1 i n. We use CO-LSNNF to denote the subset of NNF in which any formula satisfies CO-logical separability property. For instance, the formula x x is CO-logically separable as the logical contradiction occurs explicitly. To avoid the implicit logical contraditions in an unsatisfiable -node β1 βn, Definition 4 requires some conjuncts βi to be unsatisfiable and CO-logically separable.

Let us consider the formula α = ((x x) y) . The logical contradiction hidden in the inner -node x x does not impede the correctness of the procedure CO due to the occurrence of in the outermost -node of α. In a similar way, each disjunct of an unsatisfiable -node is unsatisfiable and CO-logically separable. Hence, we obtain the soundness of the procedure CO.

Theorem 2. A language L is CO-LSNNF iff the procedure CO is CO-complete and CO-sound for L.

Proof. We prove by induction on α. We here only verify the case where α is an -node β1 βn. ( ): It directly follows from Theorem 1 that the procedure CO is complete for CO-LSNNF. It remains to verify the soundness property of the procedure CO for CO-LSNNF. Let α be an arbitrary CO-LSNNF formula. Assume that CO(α) = 0. We hereafter prove that CO(α) = 0. By CO-logical separability property, there is some βi that is unsatisfiable and COls. By the induction hypothesis, we have that CO(βi) = 0. It follows from the procedure CO that CO(α) = 0. ( ): Assume that the language L is such that for any Lformula α, CO(α) = 1 iff CO(α) = 1. In case where α is satisfiable, by Definition 4, it holds that α CO-LSNNF. In case where α is unsatisfiable. By the assumption above, we get that CO(α) = 0. According to the procedure CO, we get that CO(βi) = 0 for some i. Since the procedure CO is complete, CO(βi) = 0. It follows that βi L. By the induction hypothesis, βi is CO-logically separable. By Definition 4, α is also CO-logically separable.

We observe that all normal forms, summarized in (Darwiche and Marquis 2002), supporting CO include PI, DNNF, OBDD and so on. Interestingly, they are either PI or a subset of DNNF. In addition, we observe that every formula of PI or DNNF satisfies CO-logical separability.

Proposition 1. The languages DNNF and PI are subsets of CO-LSNNF.

On the one side, -decomposability forbids simultaneous occurrence of the same variable in distinct conjuncts of any -node. Hence, no implicit logical contradiction occurs in -nodes of a DNNF-formula. On the other side, PI requires that any implicate of α is derived by a clause c of α and that no implicate c = c of α such that c |= c. The Boolean constant is a disjunction of an empty set of literals. If α implies , then it must be itself. The logical contradiction therefore appears explicitly in any unsatisfiable PI-formula. Someone may wonder if the two properties polytime satisfiability check and CO-logical separability are essentially equivalent? The four normal forms: KROM[ ], HORN[ ], ren H[ ] and K/H[ ], which supports polytime satisfiability check (Fargier and Marquis 2014), are counterexamples for the above question. As mentioned before, the formula x x is not CO-logically separable. Clearly, it is a formula of the above four normal forms. The story does not come to the end. We connect these two properties via polytime translation.

Theorem 3. A language L satisfies CO iff it is polynomially translatable into CO-LSNNF.

Proof. ( ): Assume that L supports polytime satisfiability check. We design an algorithm transforming any L-formula α into an equivalent one that is CO-logically separable. If it is satsifiable, then it is CO-logically separable; otherwise, the algorithm returns which is CO-logically separable. Since the satisfiability of L-formula α can be achieved in time polynominal in |α|, the above algorithm is also polytime. ( ): Let f be the polytime algorithm that transforms any L-formula α into an equivalent one that is CO-logically separable. By the completeness and soundness of the procedure CO for CO-LSNNF, α is satisfiable iff CO(f(α)) = 1. This, together with the fact that f and CO are polytime, imply that L satisfies CO.

In other words, L supports polytime satisfiability check iff the implicit logically contraditions in any L-formula α that are witnesses to refute the satisfiability of α can be efficiently discovered. We close this section by comparing CO-LSNNF and NNF in terms of succinctness and polynomial-translation.

Proposition 2.

NNF s CO-LSNNF NNF p CO-LSNNF and CO-LSNNF p NNF.

As mentioned in (Fargier and Marquis 2014), the inclusion p s holds. It means that there are two languages L1 and L2 such that L1 s L2 holds but L1 p L2 does not. However, they do not provide two languages confirming the inclusion p s. We have surveyed the existing literature regarding succinctness among various propositional representations (Darwiche and Marquis 2002; Wachter and Haenni 2006; Pipatsrisawat and Darwiche 2008; Fargier and Marquis 2009; Darwiche 2011; Fargier and Marquis 2014; Berre et al. 2018; Cepek and Chrom y 2020). We find that in these literature, for every two languages L1 and L2, if the succinctness relation L1 s L2 holds, then the polynomialtranslation relation L1 p L2 also holds. To the best of our knowledge, this paper is the first one to provide the pair of languages which is a witness to the inclusion p s. A classical knowledge compilation result in (Selman and Kautz 1996) states that unless PH collapses, there does not exist a class L of formulas s.t. every NNF-formula has a polysize equivalent L-formula, and L supports polytime clausal entailment. It is well-known that both CE and CO tasks for NNF are reasoning problems with high computational complexity, which are co NP-complete and NP-complete, respectively. In this paper, we show that CO-LSNNF is the language that supports polytime satisfiability check and that is equivalent succinct to NNF, proving the similar result in (Selman and Kautz 1996) for satisfiability check does not hold. Finally, determining if an NNF-formula is CO-logically separable is the same as hard as the satisfiability problem.

Proposition 3. Deciding if an NNF-formula is in CO-LSNNF is NP-complete.

Proof. (Lower bound): By CO-logically separability and Theorem 2, we get that for any NNF formula α, α is satisfiable iff α is in CO-LSNNF and CO(α) = 1. Due to the

fact that the satisfiability problem of any NNF-formula is NPcomplete, we can draw a conclusion that deciding if an NNFformula is in CO-LSNNF is NP-hard. (Upper bound): It is easy to verify that for any NNF formula α, α is in CO-LSNNF iff α is satsifiable or CO(α) = 0. The satisfiability problem is in NP and so is the CO-LSNNF membership problem.

Clausal Entailment

As mentioned in (Darwiche and Marquis 2002), a language qualifies as a target language, if it permits polytime clausal entailment check. In this section, we consider logical separability in the query clausal entailment.

The Procedure for Clausal Entailment

Definition 5. Let α be an NNF-formula and c a non-trivial clause. The procedure CE(α, c) is recursively defined as:

CE( , c) = 1, if c = 0, otherwise CE( , c) = 1, CE(l, ) = 1 and CE(l, ) = 0

CE(l, l1 lm) = 1, if l = li for some i 0, otherwise CE(β1 βn, c) = max 1 i n{CE(βi, c)}

CE(β1 βn, c) = min 1 i n{CE(βi, c)}

The above procedure is a recursive algorithm. In the case that α is a Boolean constant , the procedure returns 1 if the clause c is also , and returns 0 otherwise. In the case that α is , the procedure always returns 1 since an unsatisfiable KB derives any consequence. In the case that α is a literal l, then the procedure returns 1 if l is a literal of the clause c, or c is since l entails a clause including l and is a consequence of any formula. The clausal entailment problem of an -node β1 βn and a clause c can be reduced to the same subproblem of βi and c. If one of the βi s entails c, then their conjunction does. The case that α is a -node is similarly handled. Darwiche (2001a) proposed a polytime clausal entailment procedure CE via the procedure CO and conditioning. The definition of CE is as follows: CE (α, c) = 1 iff CO(α|t) = 0 where t is equivalent to c. In fact, the two procedures CE and CE are equivalent, that is, they return the same result for every formula α and every non-trivial clause c.

Proposition 4. Let α be an NNF-formula and c a non-trivial clause. Then, CE(α, c) = CE (α, c).

The major advantage of the procedure CE over CE is that the former directly solves the clausal entailment problem while the latter resorts to two procedures for satisfiability check and conditioning.

Definition 6. Let L be a language and f be a procedure that takes an NNF-formula α and a non-trivial clause c as input, and that returns a Boolean value. We say

f is CE-sound for L iff for every L-formula α and every non-trivial clause c, f(α, c) = 1 only if CE(α, c) = 1;

f is CE-complete for L iff for every L-formula α and every non-trivial clause c, CE(α,c)=1 only if f(α,c)=1.

The procedure CE is a sound algorithm for clausal entailment and takes polytime in the size of α and c.

Theorem 4. The procedure CE is CE-sound for NNF with the time complexity O(|α| |c|).

However, it is not guaranteed that the procedure CE is complete if α is an arbitrary NNF-formula. Let us consider the formula α = ( x y) ( y z) and the clause c = x z. It is easily verified that CE( x, c) = 1, CE(y, c) = 0, CE( y, c) = 0 and CE(z, c) = 1. It follows that CE( x y, c) = 0 and CE( y z, c) = 0. Finally, CE(α, c) = 0. On the contrary, CE(α, c) = 1 as α |= c. The reason that the procedure CE cannot give a complete answer for clausal entailment is similar to why the CO does not work perfectly for satisfiability check. The procedure CE only decomposes -nodes of a formula α in a simple way and does not reasoning about implicit logical implicate of these -nodes. We say an -node α = β1 βn contains an implicit logical implicate, if there is a clause c s.t. α |= c and βi |= c for every 1 i n. By conjoining α with the clause x z, the new formula α = ( x y) ( y z) ( x z) contains no implicit logical implicates. We now examine the procedure CE for the formula α , which is equivalent to the previous one α. It is easily verified that CE( x z, c) = 1, and hence CE(α , c) = 1. The procedure CE(α , c) generates a result in accordance with CE(α , c). Based on the above observations, we hereafter give a normal form that is the sufficient and necessary condition of making the procedure CE not only sound but also complete.

Definition 7. Let c be a non-trivial clause. An NNF-formula α is CE-logically separable (CEls) w.r.t. c iff

α is , , or a literal l; or α is an -node β1 βn, and if α |= c, then there is a conjunct βi s.t. βi |= c and βi is CEls w.r.t. c; or α is an -node β1 βn, and if α |= c, then for every disjunct βi, we have βi |= c and βi is CEls w.r.t. c.

The Boolean constants and a literal l are CEls w.r.t. any non-trivial clause c. Suppose that α is an -node β1 βn which entails a clause c. The clause c may be an implicit logical implicate of α. To avoid them, Definition 7 requires some of its conjunct to entail c and to be CE-logically separable w.r.t. c. In the similar way, if a -node entails clause c, then each of its disjuncts also entails c and is CE-logically separable w.r.t. c. We say an NNF-formula satisfies general CE-logically separable (general CEls), if it is CEls w.r.t. every non-trivial clause. We use CE-LSNNF to denote the subset of NNF for which every formula satisfies general CEls. General CE-logical separability eliminates any implicit implicate of some -nodes so as to gain the completeness of the procedure CE for every formula and every non-trivial clause.

Theorem 5. A language L is CE-LSNNF iff the procedure CE is CE-complete and CE-sound for L.

Proof. We prove by induction on α. We here only verify the case where α is an -node β1 βn. ( ): By Theorem 4, the procedure CE is CE-sound for CE-LSNNF. It remains to verify the completeness property of the procedure CE for CE-LSNNF. Let α be an arbitrary CE-LSNNF-formula and c a non-trivial clause. Assume that α |= c. We hereafter prove that CE(α, c) = 1. By CE-logical separability property, we have that βi |= c and βi is CEls w.r.t. c for some i. By the induction hypothesis, it holds that CE(βi, c) = 1. It follows from the procedure CE that CE(α, c) = 1. ( ): Assume that the language L is such that for every L-formula α and every non-trivial clause c, CE(α, c) = 1 iff CE(α, c) = 1. We prove that every L-formula α is CElogically separable w.r.t. every non-trivial clause c. In case where α |= c, by Definition 7, it holds that α is CEls w.r.t. c. In case where α |= c. By the assumption above, we get that CE(α, c) = 1. According to the procedure CE, we get that CE(βi, c) = 1 for some i. Since the procedure CE is sound for any NNF-formula, we have that CE(βi, c) = 1. It follows that βi L. By the induction hypothesis, βi is CE-logically separable w.r.t. c. By Definition 7, α is CEls w.r.t. c.

We observe that -decomposability and prime implicates are special cases of general CE-logical separability.

Proposition 5. DNNF and PI are subsets of CE-LSNNF.

We elaborate the intuition behind -decomposability and prime implicant via the inference rule: resolution. Resolution is used to find a refutation proof of CNF-formulas (Davis and Putnam 1960). Levesque (1998) used resolution to discover implicit implicates hidden in -nodes. The conjunction of x c1 and x c2 deduces their resolvant c1 c2. This deduction also holds if the two clauses c1 and c2 are replaced by two arbitrary formulas β1 and β2 respectively. On the one side, -decomposability precludes the case that a variable x simultaneously occurs in different conjuncts of an -node α. This causes no occurrence of implicit implicate within any -node. On the other side, PI-formula α requires every resolution among every two clauses of α to be entailed by a clause within α. Hence, no implicit implicate occurs via making advantage of resolution. It is easily verified that every language L that is polynomially translatable into CE-LSNNF also satisfies CE.

Theorem 6. If a language L is polynomially translatable into CE-LSNNF, then L satisfies CE.

But the opposite direction remains open. Considering the four disjunctive closure based languages, none of these languages is at least as succinct as CE-LSNNF. Any KROMformula can be converted into a PI-formula in polytime (Marquis 2000). In addition, PI is a subset of CE-LSNNF and CE-LSNNF supports polytime disjunction ( C), which will be shown in Table 1. We therefore obtain that KROM[ ] is polynomially translatable to CE-LSNNF. So CE-LSNNF is strictly more succinct than KROM[ ]. The problem whether CE-LSNNF is at least as succinct as ren H[ ], K/H[ ] and HORN[ ] remains unknown. Every CO-LSNNF-formula is an NNF-formula that is CElogically separable w.r.t. . So CO-LSNNF s CE-LSNNF. But

the opposite direction does not hold unless PH collapses.

Proposition 6. CO-LSNNF s CE-LSNNF and CE-LSNNF s CO-LSNNF.

CO-LSNNF does not support polytime conditioning which will be shown in Table 1. The following proposition states that CE-LSNNF is the maximal fragment of CO-LSNNF closed under conditioning.

Proposition 7. An NNF-formula α CE-LSNNF iff α CO-LSNNF and α|t CO-LSNNF for every non-trivial term t.

Proof. We prove by induction on α. We here only verify the case where α is an -node β1 βn. ( ): Suppose that α CE-LSNNF. Clearly, α CO-LSNNF. It remains to verify that α|t is COls for every nontrivial term t. Let c be a non-trivial clause equivalent to t. By Definition 4, if α |= c, then α|t is satisfiable, and hence α|t CO-LSNNF. We now assume that α |= c. By Definition 7, there is a conjunct βi of α s.t. βi |= c and βi is CEls w.r.t. c. By the induction hypothesis, we have βi|t is COls. By Definition 4, it holds that α|t is COls. ( ): Let α L. By assumption, α is CO-logically separable and α|t is also CO-logically separable for every nontrivial term t. Let c a non-trivial clause and t a non-trivial term equivalent to c . It remains to verify that α is CEls w.r.t. c . α is an -node β1 βn: If α|t is satisfiable, then α |= c . It follows from Definition 7 that α is CEls w.r.t. c . We now assume that α|t is unsatisfiable. By Definition 4, there is a conjunct βi of α s.t. βi|t is unsatisfiable. By the induction hypothesis, we have that βi is CEls w.r.t. c . Hence, α is CEls w.r.t. c .

The following proposition provides the upper bound of the CE-LSNNF membership problem.

Proposition 8. Deciding if an NNF-formula is in CE-LSNNF is in Πp 2.

Proof. We first consider the non-membership problem of CE-LSNNF. An NNF-formula α is not a CE-LSNNF-formula iff there exists a non-trivial clause c s.t. CE(α, c) = 1 and CE(α, c) = 0. Since the clausal entailment problem of NNFformula is co NP-complete, the non-membership problem of CE-LSNNF can be solved by a non-deterministic Turing machine M by invoking an NP oracle that decides if CE(α, c) = 1. Hence, the non-membership problem of CE-LSNNF is in ΣP 2 , and the membership problem is in ΠP 2 .

Comparison to Levesque s Normal Form In first-order logic, Levesque (1998) defined a class for queries, namely Levesque s normal norm (LNF), such that entailment check is complete, sound and can be tractably solved for a class of knowledge base, namely proper knowledge base, which is equivalent to a possibly infinite consistent set of ground literals. Since the negation is applied to a formula, LNF is not a subset of NNF. To make a clear comparison between LNF and CE-LSNNF, we propose the NNF version of LNF, namely Levesque s negation normal norm (LNNF). We remark that every LNF-formula can be converted into a polysize equivalent one in LNNF, and vice versa.

Definition 8. An NNF-formula α is in LNNF, iff

α is , , or a literal l; or α is an -node β1 βn where for any non-trivial clause c, if α |= c, then βj |= c for some 1 j n; and βi is in LNNF for every 1 i n; or α is a -node β1 βn where for any non-trivial term t, if t |= α, then t |= βj for some 1 j n; and βi is in LNNF for every 1 i n.

We use the formula α = [(( x y) ( y z)) ] ( x z) to illustrate the distinction between CE-LSNNF and LNNF. The formula α satisfies general CE-logical separability, but is not an LNNF-formula. Let β = ( x y) ( y z). Each conjunct of β does not entail the clause x z, but β does. So β is not in LNNF. It follows that β is not in LNNF. Neither does α. From the above example, we can observe that LNNF incorporates not only a stronger constraint than CE-logical separability for -nodes but also its dual property for - nodes. The direct consequences are (1) CE-LSNNF subsumes LNNF, and (2) LNNF supports polytime term implication check. CE-LSNNF is strictly more succinct than LNNF unless PH collapses.

Proposition 9. LNNF s CE-LSNNF.

Proof. It can be shown that unless PH collapses, there does not exist a class L of formulas s.t. every DNF-formula has a polysize equivalent L-formula, and L supports polytime term implication. This, together with the fact that CE-LSNNF s DNF and LNNF supports IM (Proposition 12), impiles that LNNF s CE-LSNNF.

Model Counting We now turn to the query model counting that returns the number of models of a propositional formula. A number of key AI tasks can be reduced to the model counting problem, such as probabilistic inference (Chavira and Darwiche 2008) and constraint optimization (Bulatov 2013). We hereafter develop a unified model counting algorithm.

Definition 9. Let α be an NNF-formula, Y Var(α) and Y0 = Y \ Var(α). The procedure CT (α, Y) is recursively defined as:

CT ( ,Y)=0, CT ( ,Y)=2|Y| and CT (l,Y)=2|Y| 1

CT (β1 βn, Y) = 2|Y0| Qn i=1 CT (βi, Var(βi)) CT (β1 βn, Y) = Pn i=1 CT (βi, Y)

The above procedure works in a recursive way. The first item is for the base case. The numbers of models of , and a literal are 2|Y|, 0 and 2|Y| 1, respectively. In the induction case, the model counting problem of an -node (resp. -node) is decomposed to that of its subformula. The number of models of an -node equals to the product of the number of models of its subformula βi multiplying 2|Y0|. The number of models of a -node equals to the sum of the Y-models of its subformula βi.

Definition 10. Let L be a language and f a procedure that takes an NNF-formula α and a set of variables Y s.t. Y Var(α) as inputs, and that returns a natural number. We say f is CT-overapproximate for L iff for every L-formula α, CT(α, Y) f(α, Y); f is CT-underapproximate for L iff for every L-formula α, CT(α, Y) f(α, Y). The procedure CT is overapproximate for any NNFformula α with time linear in the size of α. Theorem 7. The procedure CT is CT-overapproximate for NNF with the time complexity O(|α|). However, the procedure CT may compute the incorrect answer for some NNF-formulas. We illustrate the reasons from the model-theoretic perspective. We first consider the -node α = β1 βn. Let Ωi be the set of Yi-models of βi where Yi = Var(βi). The Cartesian product on n sets of models Ω1, , Ωn is defined as: Ω1 Ωn = {ω1 ωn | ωi Ωi for 1 i n}. The Cartesian product may contain an inconsistent set of literals, that is, a set contains a variable x and its complement x. For example, {{x}} {{ x, y}, {x, y}} = {{x, x, y}, {x, y}} where {x, x, y} is an inconsistent set of literals. The procedure CT simply returns the product of |Ω1|, , |Ωn| and the number 2|Y0|, Therefore, CT computes an overapproximate result when the Cartesian product Ω1 Ωn contains some inconsistent sets of literals. We now consider the -node α = β1 βn. Let Ωi be the set of Y-models of βi The procedure CT simply returns the sum of |Ωi|. Therefore, CT produces an overapproximate result since a Y-interpretation may satisfy more than one disjunct of α. In the following, we identify the conditions under which the procedure CT provides the exact counting of models. We say two formulas α and β agree on common variables, if for every variable x Var(α) Var(β), we have α |= x and β |= x; or α |= x and β |= x. Definition 11. An NNF-formula is CT-logically separable (CTls) iff one of the following conditions hold α is a literal, or ; α is an -node β1 βn s.t. if α is unsatisfiable, then βi is unsatisfiable and CTls for some i; if α is satisfiable, then every βi is CTls and every two distinct βi and βj agree on common variables. α is an -node β1 βn s.t. βi βj |= for i = j and every βi is CTls. With the above constraints, no inconsistent set of literals exists in the Cartesian product on sets of models of conjuncts of -nodes. Neither common models in some distinct disjuncts of -nodes does. We use CT-LSNNF to denote the subset of NNF in which any formula satisfies CT-logical separability property. CT-LSNNF precisely capture the class of formulas that allow CT to produce a correct result. Theorem 8. A language L is CT-LSNNF iff the procedure CT is CT-overapproximate and CT-underapproximate for L.

Proof. We prove by induction on α. We here only verify the case where α is an -node β1 βn. ( ): Let α be a CT-LSNNF-formula and Y Var(α). We prove that CT (α, Y) = |Mod Y(α)| = CT(α, Y). The induction step for -node: Let β0 = , Y0 = Y \ Var(α) and Yi = Var(βi) for 1 i n. In the case where α is satisfiable. By CT-logically separability property, we get that Mod Y0(β0) Mod Y1(β1) Mod Yn(βn) does not contain an inconsistent set of literals. Hence, the union of each Yi-model of βi is a Y-model of α. By the inductive hypothesis, we get that CT (βi, Yi) = |Mod Yi(βi)| for 1 i n. So |Mod Y(α)| = Qn i=0 |Mod Yi(βi)| = 2|Y0| Qn i=1 CT (βi, Yi) = CT (α, Y). In the case where α is unsatisfiable. By CTls property and the inductive hypothesis, it is easy to verify that CT (α, Y) = |Mod Y(α)| = 0. ( ): Suppose that the language L is such that for every Lformula α and every Y Var(α), CT(α, Y) = CT (α, Y). We prove that every L-formula α is CT-logically separable. We w.l.o.g. assume that Y = Var(α). Let Yi = Var(βi) for 1 i n. In the case α is satisfiable. By the assumption CT(α, Y) = CT (α, Y), the following hold:

1. CT(βi, Yi) = CT (βi, Yi) for every 1 i n; 2. Mod Y1(β1) Mod Yn(βn) does not contain an inconsistent set of literals.

By Item 1 and the induction hypothesis, we get that each βi is CTls. By Item 2, we get that every two distinct formulas βi and βj agree on common variables. It follows from CTlogically separability property that α CT-LSNNF. In the case where α is unsatisfiable. By the assumption, we get that CT (α, Y) = CT(α, Y) = 0. By procedure CT , CT (βi, Yi) = 0 for some i. Since the CT procedure is CT-overapproximate, βi is unsatisfiable. So CT (βi, Yi) = CT(βi, Yi). By the induction hypothesis, βi is CTls. Hence, α CT-LSNNF.

Darwiche (2001b) proposed a model counting algorithm that is correct for sd-DNNF, that is, the subset of d-DNNF with the smoothness property requiring that Var(βi) = Var(βj) for each -node β1 βn of an NNF-formula. By comparison, the CT algorithm has wider scope of application and is more efficient than (Darwiche 2001b) s algorithm since CT-LSNNF is a strict superset of sd-DNNF and transforming a CT-LSNNF-formula into an equivalent sd-DNNF-formula may cause a O(|X|) blowup in size where |X| is the number of variables. We hereafter prove that d-DNNF and CT-LSNNF are polynomially equivalent.

Proposition 10. d-DNNF p CT-LSNNF.

Proof. It is easily verified that CT-LSNNF p d-DNNF. We here only prove that d-DNNF p CT-LSNNF. We can transform every CT-LSNNF-formula to an equivalent d-DNNFformula in a bottom-up manner. During the transformation, we only convert every -subnode α = Sn i=1 βi as follows. We first determine the satisfiability of α, which can be solved in polytime. If α is unsatisfiable, then is a d-DNNFformula equivalent to α. Otherwise, it follows from the CTlogically separability property that each βi is in CT-LSNNF.

Suppose that β i is the transformed d-DNNF-formula equivalent to βi with polysize in |βi|. Let L = Sn i=1[Lit(β i) (Si 1 j=1 Lit(β j))] and α = β 1|L β n|L L. Since d-DNNF is closed under conditioning (cf. Proposition 5.1 in (Darwiche and Marquis 2002)), β i|L is also d-DNNF. It is easily verified that α α and α satisfies determinism and decomposability.

To the best of our knowledge, the maximal fragment of NNF supporting polytime model counting, which is discovered in the existing literature, is d-DNNF (Darwiche 2001b). In the following, we prove a dual language, namely c-DNNF, to d-DNNF that is not a subset of CT-LSNNF but supports polytime model counting. The -decomposability property requires the sets of variables of the children of each -node to be pairwise disjoint. The covering property requires the children of each -node in a formula to be pairwise logically tautology. Cover dual decomposability NNF (c-DNNF) is the subset of NNF satisfying -decomposability and covering properties. We now design a polytime model counting procedure CT for c-DNNF. Every c-DNNF-formula α can be transformed into a d-DNNF-formula α in polytime s.t. α α via replacing any occurrence of Boolean constants (resp. ) by (resp. ), of literals l by its complement l and of connectives (resp. ) by (resp. ). For convenience, we call the d-DNNF-formula α, generated from α by the above process, the complement of α. The procedure CT

for c-DNNF is defined as CT (α, Y) = 2|Y| CT ( α, Y). Since the formula α is d-DNNF, the procedure CT produces a exact number of models of α. Hence, 2|Y| CT ( α, Y) is the correct answer for the models of α. We illustrate the fact that c-DNNF is not CT-logical separable with the formula α = (x x) y. The subformula x x of α is unsatisfiable, but neither x nor x is. It violates the requirement of unsatisfiable -nodes in CT-LSNNF, and hence is not in CT-LSNNF. However, this formula α satisfies -decomposability and covering. Finally, we prove that every language L that is polynomially translatable into CT-LSNNF also satisfies CT. But the opposite direction remains open.

Theorem 9. If a language L is polynomially translatable to CT-LSNNF, then L satisfies CT.

We close this section by providing the upper bound of the CT-LSNNF membership problem.

Proposition 11. Deciding if an NNF-formula is in CT-LSNNF is in P 2 .

Proof. It is easy to design a deterministic algorithm for the CT-LSNNF membership problem via invoking NP oracle according to the definition of CT-LSNNF-formulas (cf. Definition 11). Identify whether an NNF-formula α is in CT-LSNNF requires checking the satisfiability of some subformulas of α and the conjunction of some subformulas, and checking the entailment of some subformulas and some literals. NP oracles are used to solve the above two checking and are invoked at most O(n4) times where n is the size of α.

Figure 1: Succinctness of various normal forms. An edge L1 L2 indicates L1 <s L2 while an edge L1 L2 indicates L1 s L2. A dotted right arrow from L1 to L2 means L2 s L1 but whether L1 s L2 is unknown.

L CO VA CE IM EQ SE CT ME CO-LSNNF CE-LSNNF

L CD FO SFO BC C BC C C CO-LSNNF CE-LSNNF LNNF ? ?

Table 1: Queries and transformations for the logical separability based languages. An occurrence of indicates that L supports the query (or transformation) property; means that it is not the case unless P = NP; and ? means that whether L supports this property is unknown.

Succinctness, Queries and Transformations As pointed out in (Darwiche and Marquis 2002), succinctness, queries and transformations are three key dimensions to consider when choosing an appropriate target language for application-specific problems. In this section, we discuss the relative succinctness of logical separability based languages (CO-LSNNF, CE-LSNNF, LNNF and CT-LSNNF) compared to other languages considered in (Darwiche and Marquis 2002; Fargier and Marquis 2014) in Figure 1. We also investigate the supported queries and transformations of logical separability based languages in Table 1. Proposition 12. The results in Figure 1 and Table 1 hold. We can make several observations from Figure 1 and Table 1 as follows. (1) There are two succinctness orderings of logical separability based languages: CO-LSNNF <s CE-LSNNF <s CT-LSNNF and CO-LSNNF <s CE-LSNNF <s LNNF. CT-LSNNF s LNNF but whether LNNF s CT-LSNNF remains open. (2) Adding COlogical separability to NNF gains the polytime satisfiability check property without lowering down its succinctness hi-

erarchy. But CO-LSNNF loses the transformation properties: CD, BC, C and C which hold in NNF. It is worthy noting that CO-LSNNF is at least as succinct as any language that offers polytime satisfiability check. (3) Besides KROM[ ] and subsets of DNNF, CE-LSNNF is another fragment of NNF supporting CE, FO and C. Furthermore, CE-LSNNF is strictly more succinct than any languages supporting CE except ren H[ ], K/H[ ] and HORN[ ]. (4) Although LNNF offers VA and IM compared to CE-LSNNF, but the former is not closed under bounded disjunction and is less succinct than the latter. (5) CT-LSNNF is equally succinct to d-DNNF and hence supports the same query and transformation properties as d-DNNF. (6) None of logical separability based languages satisfies bounded conjunction.

Conclusion and Future Work

Inspired by Levesque, we introduce three new logical separability based properties: CO-logical separability, CE-logical separability and CT-logical separability for query tasks CO, CE and CT respectively, establishing the connection between knowledge compilation and logical separability. We then identify three novel fragments: CO-LSNNF, CE-LSNNF and CT-LSNNF, which precisely capture the classes of formulas that permit polytime procedures CO, CE and CT always produce a correct answer of the corresponding tasks respectively. We also extend the knowledge compilation map by investigating succinctness and tractability of the four logical separability based languages (CO-LSNNF, CE-LSNNF, LNNF and CT-LSNNF). We show that CO-LSNNF is the most succinct language permitting CO and particularly any propositional formula has a polysize equivalent CO-LSNNF formula. CE-LSNNF is as powerful as DNNF since they supports the same set of queries and transformations, yet strictly more succinct. CT-LSNNF is the same as succinct as d-DNNF and offers the same tractability as d-DNNF. There are several directions for future works. Firstly, the remaining open questions include: the unknown succinctness, supported queries and transformations which shown in Figure 1 and Table 1 as well as the lower bound of the membership problem of CE-LSNNF and CT-LSNNF. Secondly, we would like to develop a compilation method for CE-LSNNF, leading to build up a more efficient representation for two important AI problems: planning and model-based diagnosis. This is because that CE-LSNNF is the most succinct normal form, shown in Figure 1, which supports the four basic queries and transformations (clausal entailment, model enumeration, conditioning and forgetting) that are essential to planning and model-based diagnosis. Finally, it is interesting to further apply the notion of logical separability to more query and transformation tasks.

Acknowledgments

This paper was supported by the National Natural Science Foundation of China (Nos. 62077028, 61877029, 61906216, 62176103 and 61603152), the Guangdong Basic and Applied Basic Research Foundation (Nos. 2021A1515011873, 2021B0101420003, 2021B1515120048, 2020A1515010642,

2020B0909030005, 2020B1212030003, 2020ZDZX3013, 2019A050510024, 2019B1515120010 and 2018A030310633), the Specially Creative University Project of Guangdong (Nos. 2019KTSCX010 and 2018KTSCX016), the Fundamental Research Funds for the Central Universities (Nos. 11621418 and 21617349), the Science and Technology Project of Guangzhou (Nos. 202102080307, 202102021173 and 201902010041), and the Project of Guangxi Key Laboratory of Trusted Software (No. kx201604).

References Berre, D. L.; Marquis, P.; Mengel, S.; and Wallon, R. 2018. Pseudo-Boolean Constraints from a Knowledge Representation Perspective. In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI-2018), 1891 1897. Bulatov, A. A. 2013. The Complexity of the Counting Constraint Satisfaction Problem. Journal of the ACM, 60(5): 1 41. Chavira, M.; and Darwiche, A. 2008. On Probabilistic Inference by Weighted Model Counting. Artificial Intelligence, 172(6-7): 772 799. Darwiche, A. 2001a. Decomposable Negation Normal Form. Journal of the ACM, 48(4): 608 647. Darwiche, A. 2001b. On the Tractable Counting of Theory Models and its Application to Truth Maintenance and Belief Revision. Journal of Applied Non-Classical Logics, 11(1-2): 11 34. Darwiche, A. 2011. SDD: A New Canonical Representation of Propositional Knowledge Bases. In Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence (IJCAI-2011), 819 826. Darwiche, A.; and Hirth, A. 2020. On the Reasons Behind Decisions. In Proceedings of the Twenty-Fourth European Conference on Artificial Intelligence (ECAI-2020), 712 720. Darwiche, A.; and Marquis, P. 2002. A Knowledge Compilation Map. Journal of Artificial Intelligence Research, 17(1): 229 264. Davis, M.; and Putnam, H. 1960. A Computing Procedure for Quantification Theory. Journal of the ACM, 7(3): 201 215. Fargier, H.; and Marquis, P. 2009. Knowledge Compilation Properties of Trees-of-BDDs, Revisited. In Proceedings of the Twenty-First International Joint Conference on Artificial Intelligence (IJCAI-2009), 772 777. Fargier, H.; and Marquis, P. 2014. Disjunctive Closures for Knowledge Compilation. Artificial Intelligence, 216: 129 162. Horn, A. 1951. On Sentences Which are True of Direct Unions of Algebras. Journal of Symbolic Logic, 16(3): 14 21. Huang, J. 2006. Combining Knowledge Compilation and Search for Conformant Probabilistic Planning. In Proceedings of the Sixteenth International Conference on Automated Planning and Scheduling (ICAPS-2006), 253 262.

Huang, J.; and Darwiche, A. 2005. On Compiling System Models for Faster and More Scalable Diagnosis. In Proceedings of the Twentieth National Conference on Artificial Intelligence (AAAI-2005), 300 306. Krom, M. R. 1970. The Decision Problem for Formulas in Prenex Conjunctive Normal Form with Binary Disjunctions. Journal of Symbolic Logic, 35(2): 210 216. Levesque, H. J. 1998. A Completeness Result for Reasoning with Incomplete First-Order Knowledge Bases. In Proceedings of the Sixth International Conference on Principles of Knowledge Representation and Reasoning (KR1998), 14 23. Marquis, P. 2000. Consequence Finding Algorithms. In Handbook of Defeasible Reasoning and Uncertainty Management Systems, 41 145. Springer. Martires, P. Z. D.; Dries, A.; and De Raedt, L. 2019. Exact and Approximate Weighted Model Integration with Probability Density Functions using Knowledge Compilation. In Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence (AAAI-2019), 7825 7833. Mateescu, R.; Dechter, R.; and Marinescu, R. 2008. AND/OR Multi-Valued Decision Diagrams (AOMDDs) for Graphical Models. Journal of Artificial Intelligence Research, 33: 465 519. Palacios, H.; Bonet, B.; Darwiche, A.; and Geffner, H. 2005. Pruning Conformant Plans by Counting Models on Compiled d-DNNF Representations. In Proceedings of the Fifteenth International Conference on Automated Planning and Scheduling (ICAPS-2005), 141 150. Pipatsrisawat, K.; and Darwiche, A. 2008. New Compilation Languages Based on Structured Decomposability. In Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence (AAAI-2008), 517 522. Selman, B.; and Kautz, H. 1996. Knowledge Compilation and Theory Approximation. Journal of the ACM, 43(2): 193 224. Shih, A.; Choi, A.; and Darwiche, A. 2019. Compiling Bayesian Network Classifiers into Decision Graphs. In Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence (AAAI-2019), 7966 7974. Shih, A.; Darwiche, A.; and Choi, A. 2019. Verifying Binarized Neural Networks by Angluin-Style Learning. In Proceedings of the Twenty-Second International Conference on Theory and Applications of Satisfiability (SAT-2019), volume 11628, 354 370. Cepek, O.; and Chrom y, M. 2020. Properties of Switch-List Representations of Boolean Functions. Journal of Artificial Intelligence Research, 69: 501 529. Wachter, M.; and Haenni, R. 2006. Propositional DAGs: A New Graph-Based Language for Representing Boolean Functions. In Proceedings of the Tenth International Conference on Principles of Knowledge Representation and Reasoning (KR-2006), 277 285.