Existential Closures for Knowledge Compilation

1 Introduction

Knowledge compilation (KC) is concerned with preprocessing for improving the efficiency of computational tasks (see among others [Darwiche, 2001; Cadoli and Donini, 1998; Selman and Kautz, 1996; Schrag, 1996; del Val, 1994]). An important issue within this research area is the choice of a target language into which some pieces of data are to be translated during the off-line, compilation phase [Gogic et al., 1995; Darwiche and Marquis, 2002]. In [Darwiche and Marquis, 2002], the authors argue that such a choice must be based both on the set of queries and transformations which can be achieved in polynomial time once the pre-processed pieces of data are represented in the target language, as well as the succinctness of the language (i.e., its ability to represent data using few space.) The basic queries considered in [Darwiche and Marquis, 2002] include tests for consistency, validity, implicates (clausal entailment), implicants, equivalence, sentential entailment, counting and enumerating theory models (CO, VA, CE, IM, EQ, SE, CT, ME.) The basic transformations are conditioning (CD), closures under the connectives ( ∧C, ∧BC, ∨C, ∨BC, ¬C), and forgetting (FO, SFO.) The KC map given in [Darwiche and Marquis, 2002] is an evaluation of a dozen of significant propositional languages w.r.t. several criteria: the succinctness of the language and the set of queries and transformations it supports in polynomial time. Such a map can be used as a guide for targeting the "right language" given the requirements imposed by the application under consideration.

∗This research was supported by the project TUPLES-ANR-10BLAN-0210 of the French National Agency for Research - Agence Nationale de la Recherche

The KC map provided in [Darwiche and Marquis, 2002] has been extended to incorporate further propositional languages (also referred to as "fragments"), queries and transformations, see among others [Wachter and Haenni, 2006], [Fargier and Marquis, 2006], [Subbarayan et al., 2007], [Fargier and Marquis, 2008b], [Fargier and Marquis, 2008a], [Fargier andMarquis, 2009]. In [Fargier andMarquis, 2008b; 2008a] an approach to define new target languages for KC has been pointed out. It consists in applying closure principles to previous languages. [Fargier and Marquis, 2008a] consider two disjunctive closure principles: disjunction (∨) and existential closure (∃.) Intuitively, the disjunction principle when applied to a propositional language L leads to a language L[∨] which qualifies disjunctions of formulae from L, while existential closure applied to L leads to a language L[∃] which qualifies existentially quantified formulae from L. Whatever L, L[∨] satisfies polytime closure under ∨ and L[∃] satisfies polytime forgetting. Applying any/both of those two principles to L may lead to new fragments, which can prove strictly more succinct than L. Thus, [Fargier and Marquis, 2008a] locate on the KC map all languages obtained by applying those closure principles to some complete languages, i.e., languages L for which every propositional formula has an equivalent in L. Thus, the disjunctive closures of the languages OBDD< (ordered binary decision diagrams), DNF (disjunctive normal forms), DNNF (decomposable negation normal forms), CNF (conjunctive normal forms), PI (prime implicates), IP (prime implicants), MODS (models), considered in [Darwiche and Marquis, 2002], have been studied in [Fargier and Marquis, 2008a]. On the other hand, [Fargier and Marquis, 2008b] consider the disjunction closures KROM-C[∨], HORN-C[∨], K/H-C[∨], renH-C[∨], and AFF[∨], composed respectively of disjunctions of Krom CNF formulae, disjunctions of Horn CNF formulae, disjunctions of Krom or Horn CNF formulae, disjunctions of renamable Horn CNF formulae, and disjunctions of affine formulae.

Each of these languages is complete, unlike the underlying languages KROM-C (also known as the bijunctive fragment) [Krom, 1970], HORN-C [Horn, 1951], AFF (also known as the biconditional fragment) [Schaefer, 1978], K/H-C (Krom or Horn CNF formulae) and renH-C.

In the following, we complete the results reported in [Fargier and Marquis, 2008b; 2008a] by focusing on the existential closures of the ten languages KROM-C, HORN-C, K/H-C, renH-C, AFF, KROM-C[∨], HORN-C[∨], K/H-C[∨], renH-C[∨], and AFF[∨]. We evaluate each of them along the lines considered in [Darwiche and Marquis, 2002]. The contribution of the paper is mainly as follows:

• For each existential closure of KROM-C, HORN-C, K/H-C, renH-C, AFF, KROM-C[∨], HORN-C[∨], K/H-C[∨], renH-C[∨], and AFF[∨], we identify the queries and transformations which are feasible in polynomial time, and those which are not (possibly under some standard assumptions of complexity theory.)
• We demonstrate that the existential closure of each language L among the ten languages above is just as expressive as L. As to succinctness, we prove that L[∃] is strictly more succinct than L, except for L = KROM-C and L = AFF since for those two languages, L[∃] and L are polynomially equivalent.
• We complete the results about disjunction closures provided in [Fargier and Marquis, 2008b]; especially, we show that FO is not satisfied by any of HORN-C[∨], K/H-C[∨], renH-C[∨].
• We show that neither d-DNNF nor SDNNF is strictly more succinct than any disjunction closure of KROM-C, HORN-C, K/H-C, renH-C, AFF; it shows such disjunction closures (and the existential closures of them) as interesting alternatives to DNNF languages.

The rest of the paper is organized as follows: in Section 2, the queries and transformations considered in the KC map, as well as the fundamental notions of expressiveness and succinctness, are recalled. The notions of disjunctive, disjunction and existential closure are also presented. In Section 3, our new results are presented. Section 4 discusses the results and provides some perspectives. An extended version of the paper (including proofs) is available at http://www.cril.fr/∼marquis/ijcai11.pdf

2 The KCMap and Disjunctive Closures

In this paper, we consider subsets of the propositional language QDAG of quantified propositional DAGs. QDAG is given by:

Definition 1 (QDAG) Let PS be a denumerable set of propositional variables. QDAG is the set of all finite, single-rooted DAGs α where:

• each leaf node of α is labeled by a literal l over PS, or by a Boolean constant ⊤ (always true) or ⊥ (always false) ;
• each internal node of α is labeled by a connective c ∈ {∧, ∨, ¬, ⊕} and has as many children as required by c,

or is labeled by ∃x (where x ∈ PS) and has a single child.

All the propositional languages considered so far as target languages to KC are subsets of QDAG, and typically of DAG, the subset of QDAG where no node labeled by a quantification is allowed. Especially, the fragments considered in [Wachter and Haenni, 2006] are included in the subset of DAG where c is among {∧, ∨, ¬}, and the fragments considered in [Darwiche and Marquis, 2002] (especially OBDD<, DNF, DNNF, CNF, PI, IP, MODS) are subsets of DAG-NNF (the subset of the latter when ¬ is disallowed.)

A literal (over V ⊆ PS) is an element x ∈ V (a positive literal) or a negated one ¬x (a negative literal), or a Boolean constant. l is the complementary literal of literal l, so that ⊤ = ⊥, ⊥ = ⊤, x = ¬x and ¬x = x. For a literal l different from a Boolean constant, var(l) denotes the corresponding variable: for x ∈ PS, we have var(x) = x and var(¬x) = x. A clause (resp. a term) is a finite disjunction (resp. conjunction) of literals. An XOR-clause is a finite XOR-disjunction of literals (the XOR connective is denoted by ⊕.)

Each element α of QDAG is called a QDAG formula. Var(α) denotes the set of free variables x of α, i.e., those variables x for which there exists a leaf node nx of α labelled by a literal l such that var(l) = x and there is a path from the root of α to nx such that no node from it is labelled by ∃x. The size |α| of a QDAG formula |α| is the number of nodes plus the number of arcs in the DAG.

Figure 1 presents a QDAG formula. Its set of free variables is {q, r}. The DAG rooted at the ∧ node is a DAG formula and the DAG rooted at the ∨ node is a DAG-NNF formula.

In the following, we consider the next queries and transformations:

Definition 2 (queries) Let L⊆ QDAG.

• L satisfies CO (resp. VA) iff there exists a polytime algorithm that maps every formula α from L to 1 if α is consistent (resp. valid), and to 0 otherwise.

• L satisfies CE iff there exists a polytime algorithm that maps every formula α from L and every clause γ to 1 if α |= γ holds, and to 0 otherwise.
• L satisfies EQ (resp. SE) iff there exists a polytime algorithm that maps every pair of formulae α, β from L to 1 if α ≡ β (resp. α |= β) holds, and to 0 otherwise.
• L satisfies IM iff there exists a polytime algorithm that maps every formula α from L and every term γ to 1 if γ |= α holds, and to 0 otherwise.
• L satisfies CT iff there exists a polytime algorithm that maps every formula α from L to a nonnegative integer that represents the number of models of α over V ar(α) (in binary notation.)
• L satisfies ME iff there exists a polynomial p(., .) and an algorithm that outputs all models of an arbitrary formula α from L in time p(n,m), where n is the size of α and m is the number of its models (over V ar(α).)
• L satisfies MC (model checking) iff there exists a polytime algorithm that maps every formula α from L and every interpretation ω over V ar(α) (represented as a term) to 1 if ω is a model of α, and to 0 otherwise.

Definition 3 (transformations) Let L⊆ QDAG.

• L satisfies CD iff there exists a polytime algorithm that maps every formula α from L and every consistent term γ to a formula from L that is logically equivalent to the conditioning α | γ of α on γ, i.e., the formula obtained by replacing each free occurrence of variable x of α by ⊤ (resp. ⊥) if x (resp. ¬x) is a positive (resp. negative) literal of γ.
• L satisfies FO iff there exists a polytime algorithm that maps every formula α from L and every subset X of variables from PS to a formula from L equivalent to ∃X.α. If the property holds for each singleton X, we say that L satisfies SFO.
• L satisfies ∧C (resp. ∨C) iff there exists a polytime algorithm that maps every finite set of formulae α1, . . . , αn from L to a formula of L that is logically equivalent to α1 ∧ . . . ∧ αn (resp. α1 ∨ . . . ∨ αn.)
• L satisfies ∧BC (resp. ∨BC) iff there exists a polytime algorithm that maps every pair of formulae α and β from L to a formula of L that is logically equivalent to α ∧ β (resp. α ∨ β.)
• L satisfies ¬C iff there exists a polytime algorithm that maps every formula α from L to a formula of L logically equivalent to ¬α.

We also consider the following notions of expressiveness and succinctness:

Definition 4 (expressiveness) Let L1 and L2 be two subsets of QDAG. L1 is at least as expressive as L2, denoted L1 ≤e L2, iff for every formula α ∈ L2, there exists an equivalent formula β ∈ L1.

Definition 5 (succinctness) Let L1 and L2 be two subsets of QDAG. L1 is at least as succinct as L2, denoted L1 ≤s L2, iff there exists a polynomial p such that for every formula

α ∈ L2, there exists an equivalent formula β ∈ L1 where |β| ≤ p(|α|).

Finally, we take advantage of the following restriction of the succinctness relation:

Definition 6 (polynomial translation) Let L1 and L2 be two subsets of QDAG. L1 is said to be polynomially translatable into L2, noted L1 ≥p L2, iff there exists a polytime algorithm f such that for every α ∈ L1, we have f(α) ∈ L2 and f(α) ≡ α.

Whenever L1 is polynomially translatable into L2, every query which is supported in polynomial time in L2 also is supported in polynomial time in L1; and conversely, every query which is not supported in polynomial time in L1 unless P = NP (resp. unless the polynomial hierarchy PH collapses) cannot be supported in polynomial time in L2, unless P = NP (resp. unless PH collapses.)

∼e is the symmetric part of ≤e defined by L1 ∼e L2 iff L1 ≤e L2 and L2 ≤e L1. <e is the asymmetric part of ≤e defined by L1 <e L2 iff L1 ≤e L2 and L2 ̸≤e L1. Similarly, ∼s (resp. ∼p) is the symmetric part of ≤s (resp. ≤p.) <s (resp. <p) is the asymmetric part of ≤s (resp. ≤p.) When L1 ∼p L2, L1 and L2 are said to be polynomially equivalent. Obviously enough, polynomially equivalent fragments are equally efficient (and succinct) and possess the same set of tractable queries and transformations.

We are now ready to present disjunctive closures. Intuitively, a closure principle applied to a propositional fragment L defines a new propositional language, called a closure of L, through the application of "operators" (i.e., connectives or quantifications.) The resulting closure is said to be disjunctive when the operators are among ∨ and ∃x with x ∈ PS. Formally:

Definition 7 (disjunctive closures) Let L ⊆ QDAG and △ ⊆ {∨, ∃}. The closure L[△] of L by △ is the subset of QDAG inductively defined as follows: 1

1. if α ∈ L, then α ∈ L[△],
2. if ∨ ∈ Δ and αi ∈ L[△] for each i ∈ 1, . . . , n, then ∨(α1, . . . , αn) ∈ L[△],
3. if ∃ ∈ Δ, x ∈ PS, and α ∈ L[△], then ∃x.α ∈ L[△].

Thus, an element of L[△] can be viewed as a "tree" which "internal nodes" are labelled by quantifications of the form ∃x or by ∨ and its "leaf nodes" are labelled by elements of L. Accordingly, the formulae αi considered in item 2. of Definition 7 do not share any common subgraphs.

The set D(L) (resp. ∨(L), ∃(L)) of all disjunctive (resp. disjunction, existential) closures of a subset L of QDAG is defined inductively by:

• L belongs to D(L) (resp. ∨(L), ∃(L));
• If L belongs to D(L) (resp. ∨(L), ∃(L)) and △ ⊆ {∨, ∃} (resp. △ ⊆ {∨}, △ ⊆ {∃}), then L[△] belongs to D(L) (resp. ∨(L), ∃(L).)

1 In order to alleviate the notations, when △ = {δ1, . . . , δn}, we write L[δ1, . . . , δn] instead of L[{δ1, . . . , δn}].

[Fargier and Marquis, 2008a] provide several generalscope characterization results for disjunctive closures. Especially, they show that for a given L ⊆ DAG, only three disjunctive closures are worth to be considered since L[∃][∃] = L[∃], L[∨][∨] = L[∨] and L[∃][∨] ∼p L[∨][∃] ∼p L[∨, ∃] (see item 4. of Proposition 1 and item 1. of Proposition 2 in [Fargier and Marquis, 2008a].) They also study the disjunctive closures of the languages OBDD<, DNF, DNNF, CNF, PI, IP, MODS considered in [Darwiche and Marquis, 2002].

3 Analyzing New Existential Closures

[Fargier and Marquis, 2008b] focus on the disjunction closures of the following incomplete fragments:

Definition 8 (some incomplete fragments)

• KROM-C is the subset of CNF consisting of formulae in which each clause is binary, i.e., it contains at most two literals.
• HORN-C is the subset of CNF consisting of formulae in which each clause is Horn, i.e., it contains at most one positive literal.
• K/H-C is the union of KROM-C and HORN-C.
• renH-C is the subset of CNF consisting of formulae α for which there exists a subset V of Var(α) (called a Horn renaming for α) such that the formula V (α) obtained by substituting in α every literal l over V by its complementary literal l is a HORN-C formula. 2
• AFF is the subset of DAG consisting of conjunctions of XOR clauses.

In the following, we complete the results provided in [Fargier and Marquis, 2008b] by studying the queries, transformations, expressiveness and succinctness of the existential closures of the propositional fragments considered in [Fargier and Marquis, 2008b], i.e., we consider the languages KROM-C[∃], HORN-C[∃], K/H-C[∃], renH-C[∃], AFF[∃], KROM-C[∨, ∃], HORN-C[∨, ∃], K/H-C[∨, ∃], renH-C[∨, ∃], AFF[∨, ∃].

Figure 2 presents a HORN-C[∨, ∃] formula equivalent to the CNF formula (¬p ∨ ¬r) ∧ (¬r ∨ ¬s) ∧ (¬q ∨ ¬s).

We know that each of KROM-C and AFF satisfies FO [Fargier and Marquis, 2008b]. Furthermore, for any L ⊆ DAG, if L satisfies FO, then L[∨] satisfies FO as well. As a consequence, we immediately get that

• KROM-C[∃] ∼p KROM-C, and AFF[∃] ∼p AFF,
• KROM-C[∨, ∃] ∼p KROM-C[∨], and AFF[∨, ∃] ∼p AFF[∨].

Since KROM-C, AFF, KROM-C[∨], and AFF[∨] have been studied in [Fargier and Marquis, 2008b], we mainly focus on HORN-C[∃], K/H-C[∃], renH-C[∃], HORN-C[∨, ∃], K/H-C[∨, ∃], renH-C[∨, ∃] in the following.

2 Note that there exists linear time algorithms for recognizing renH-C formulae (see e.g. [del Val, 2000]); furthermore, such recognition algorithms typically give a Horn renaming when it exists.

As to queries and transformations, we have obtained the following results:

Proposition 1 The results given in Table 1 and in Table 2 hold.

As to expressiveness, it turns out that for any language L among K/H-C, HORN-C, renH-C, K/H-C[∨], HORN-C[∨], renH-C[∨], going from L to L[∃] does not lead to a shift:

Proposition 2 For every L among K/H-C, HORN-C, renH-C, K/H-C[∨], HORN-C[∨], renH-C[∨], we have L ∼e L[∃].

As a consequence (see [Fargier and Marquis, 2008b]), we have HORN-C[∨, ∃] ∼e K/H-C[∨, ∃] ∼e renH-C[∨, ∃]: these three languages are just equally expressive since they are complete for propositional logic (just observe that the complete language DNF is a subset of each of them.) Contrastingly, each of HORN-C[∃], K/H-C[∃], renH-C[∃] is strictly less expressive than any complete language.

Furthermore, we have:

while HORN-C[∃] and KROM-C[∃] are incomparable w.r.t. ≤e (and AFF[∃], which is polynomially equivalent to AFF, is incomparable w.r.t. ≤e with any of the three incomplete fragments above.)

As to succinctness, the picture is rather different. Typically going from L to L[∃] leads to a a succinctness increase:

Proposition 3

1. None of CNF or DNF is at least at succinct as any of HORN-C[∃], K/H-C[∃] or renH-C[∃].
2. AC3 , the language containing all disjunctions of CNF formulae and all conjunctions of DNF formulae, is not at least as succinct as any of HORN-C[∨, ∃], K/H-C[∨, ∃] and renH-C[∨, ∃].

Since HORN-C (resp. K/H-C, renH-C) is a subset of both CNF and HORN-C[∃] (resp. K/H-C[∃], renH-C[∃]), item 1. of Proposition 3 shows that going from L to L[∃] for any of these three languages leads to a strictly more succinct language. Furthermore, since HORN-C[∨] (resp. K/H-C[∨], renH-C[∨]) is a subset of both AC3 and HORN-C[∨, ∃] (resp. K/H-C[∨, ∃], renH-C[∨, ∃]), item 2. of Proposition 3 shows that a similar conclusion can be drawn for those three languages, namely HORN-C[∨] (resp. K/H-C[∨], renH-C[∨]) is strictly less succinct than HORN-C[∨, ∃] (resp. K/H-C[∨, ∃], renH-C[∨, ∃].) As a by-product, this shows that for sure, none of HORN-C[∨], K/H-C[∨], renH-C[∨] satisfies FO, an issue left open in [Fargier and Marquis, 2008b].

Finally, we have also compared the disjunction closures of KROM-C, HORN-C, K/H-C, renH-C, AFF, PI with the two main subsets of DNNF, namely the set d-DNNF of deterministic DNNFs and the set SDNNF of structured DNNFs (the union for all vtrees T of all DNNF languages DNNFT respecting T) (see [Pipatsrisawat and Darwiche, 2008] for details.) What makes those subsets so significant is that every available compilation algorithm which outputs a DNNF formula actually computes a d-DNNF formula [Darwiche, 2001; 2004] or a SDNNF formula [Pipatsrisawat and Darwiche, 2008; 2010]. First of all, as an easy consequence of the fact that DNNF is not at least as succinct as DNF, unless PH collapses, we have that:

Proposition 4 d-DNNF is not at least as succinct as any language among the existential closures of KROM-C[∨], HORN-C[∨], K/H-C[∨], renH-C[∨], AFF[∨], PI[∨], and OBDD<[∨], unless PH collapses.

This shows those existential closures as interesting alternatives to d-DNNF for applications where FO, ∨C (and for some of them ∧BC) are required since such closures offer them while d-DNNF does not (the price to be paid is that VA, IM and CT are lost while they are offered by d-DNNF.)

As to SDNNF, we have got that:

Proposition 5 SDNNF is not at least as succinct as any language among the disjunctive closures of KROM-C, HORN-C, K/H-C, renH-C, AFF, PI, and CNF.

Thus, every language that is at most as succinct as SDNNF is not at least as succinct as any disjunctive closure of KROM-C, HORN-C, K/H-C, renH-C, AFF, PI, CNF. This includes in particular OBDD<, OBDD<[∨], the language O-DDG of Ordered Decomposable Decision Diagrams [Fargier and Marquis, 2006], and the language AOMDD of AND/OR Multi-Valued Decision Diagrams (restricted to propositional variables) [Mateescu et al., 2008] (or equivalently the language SO-DDG of Strongly Ordered Decomposable Decision Diagrams [Fargier and Marquis, 2006].)

4 Conclusion and Perspectives

In this paper, we have studied the existential closures of both incomplete languages (KROM-C, HORN-C, K/H-C, renH-C, and AFF) and complete languages (the corresponding disjunction closures KROM-C[∨], HORN-C[∨], K/H-C[∨], renH-C[∨], and AFF[∨].) The results given above show that for each complete language L under consideration, the corresponding existential closure L[∃] is at least as good as L as a target language for KC. Indeed, L and L[∃] satisfy the same queries and when L does not satisfy FO, L[∃] offers it for free and is equally expressive but strictly more succinct than L. For the incomplete languages considered here, namely KROM-C, HORN-C, K/H-C, renH-C, AFF, the same conclusions can be drawn as to transformations, expressiveness and succinctness; the price to be paid for getting FO for free and obtaining a strictly more succinct language is paid by the loss of the EQ and SE queries when the existential closures of HORN-C, K/H-C, renH-C are considered.

Our study also shows HORN-C[∨, ∃] as a valuable complete target language for the KC purpose. Indeed, HORN - C[∨, ∃] satisfies the same queries and transformations as DNNFT or AFF[∨] (which is polynomially equivalent to AFF[∨, ∃].) Especially, HORN-C[∨, ∃] satisfies ∧BC and this paves the way for bottom-up compilation algorithms targeting HORN-C[∨, ∃]. As noted in [Pipatsrisawat and Darwiche, 2008], this is important for applications from formal verification based on unbounded model checking which require bottom-up, incremental compilation of formulae, where pieces of the knowledge base are compiled independently and then conjoined together. 3 Furthermore, HORN-C[∨, ∃] guarantees some polynomial-sized representations for families of propositional formulae, like the CNF representations of circular bit shift functions (resp. the CNF formulae αn = ∧ni=1 (¬xi ∨ ¬yi)), which have only exponential-sized SDNNF representations (resp. exponential-sized AFF[∨] representations, see [Fargier and Marquis, 2008b].) Compared to d-DNNF, while it does not satisfy the queries VA, IM and CT, HORN-C[∨, ∃] offers the transformations FO, ∨C and ∧BC. Finally, d-DNNF is not at least as succinct as HORN - C[∨, ∃] unless PH collapses.

From the practical side, it is important to note that some empirical evidence in favour of HORN-C[∨, ∃] compilations and renH-C[∨, ∃] already exists. On the one hand, [Nishimura et al., 2004] (resp. [Samer and Szeider, 2008]) have shown that the problem of determining whether a given CNF formula α has a strong HORN-C-backdoor set (resp. a HORN-C-backdoor tree) containing at most k variables (resp. leaves) is fixed-parameter tractable with parameter k. Interestingly, the algorithm given in [Samer and Szeider, 2008] can be used to determine "efficiently"(i.e., for sufficiently "small" k) whether a HORN - C[∨] compilation of reasonable size (i.e., linear in k and the size of α) exists. As mentioned in [Samer and Szeider, 2008]: "There is some empirical evidence that real-world instances actually have small backdoor sets". On the other hand, [Boufkhad et al., 1997] present some compilation algorithms targeting respectively HORN-C[∨] and renH-C[∨], and evaluate them on a number of benchmarks. While such results show the feasibility of HORN - C[∨, ∃] compilation and renH - C[∨, ∃] compilation, we can hardly use those results to compare the two target fragments HORN-C[∨, ∃] and renH-C[∨, ∃] with OBDD< and DNNF for which some experimental results are also available. Indeed, the compilation algorithms given in [Boufkhad et al., 1997] are based on an old-style DPLL SAT solver, and the performances of such solvers are dramatically overtaken by those of modern SAT solvers, based on a CDCL architecture. Accordingly, the main perspective of this work is to develop and evaluate compilation algorithms based on a CDCL SAT solver, and which target HORN - C[∨, ∃] and renH - C[∨, ∃].

3 Since HORN - C[∨, ∃] satisfies CO and CL (i.e., every propositional clause has a polynomial-sized representation in the language), getting ∧BC is optimal in the sense that no propositional language can satisfy both ∧C, CO, and CL, unless P = NP.

Acknowledgments

The author would like to thank the anonymous reviewers for their helpful comments.