Pseudo-Boolean Constraints from a Knowledge Representation Perspective

1 Introduction

Many applications in AI are based on propositional information. When dealing with such applications, an important issue is thus choosing a representation from a given language, for the information that is suited to the way that the information is processed [Gogic et al., 1995]. However there exist dozens of languages for representing propositional information.

The large number of candidate languages is explained by the fact that there is no single language that is the best for all potential tasks to be achieved on propositional information. Indeed, the "right" choice typically depends on the way the information is primarily reported and on the efficiency of the computations which must be made on it for the application at hand. Thus, one needs to consider selection criteria to make an informed choice [Darwiche and Marquis, 2002].

In many cases, propositional information represents laws or constraints which must be aggregated conjunctively. In such cases, the language CNF consisting of conjunctions of propositional clauses is often used. Thus, many benchmarks corresponding to various AI applications (and many applications outside the AI area as well) are encoded as CNF formulae, most often in the standard DIMACS format [DIMACS, 1993]. The focus on CNF is justified by the fact that clauses are basic objects, which can be interpreted as very simple if-then rules, and encoded and handled in a straightforward way (as lists of literals). Moreover, there is a rich ecosystem around CNF formulae with preprocessors, solvers and benchmark instances from many fields, see e.g. [SATLIB, 1999; Biere et al., 2009]. However, CNF suffers from some weaknesses. Clauses are somewhat too simple to express some important constraints. For instance, it is shown in [Dixon, 2004] that stating that, in a given set of m variables, at least n of them must be set to true cannot be carried out using a number of clauses that is polynomial in n in general without adding any new variables, which is undesirable in some settings (see the conclusion of the paper). In order to encode such constraints in a compact way, generalizations of the clause representation have been considered, in particular the so-called pseudo-Boolean constraints (linear equations or inequalities over literals), strongly related to threshold functions [Crama and Hammer, 2011], and their special case cardinality constraints (pseudo-Boolean constraints where each literal has a coefficient equal to one). These two constraints regularly arise naturally in many settings. Obviously enough, any clause ∨ki=1 li can be turned in linear time into an equivalent cardinality constraint of the form ∑ki=1 li ≥ 1 so all information represented by a CNF formula can easily be transformed into a cardinality constraint representation.

Pseudo-Boolean constraints have also attracted attention due to associated proof systems, like the cutting planes system, that have been introduced for proving the inconsistency of a conjunction of such constraints [Cook et al., 1987; Hooker, 1988; Nordstr¨om, 2015]. The cutting planes proof system is known to p-simulate the well-known resolution proof system, the underlying of modern SAT solvers, which means that there exists a fixed polynomial p such that every refutation of size l in the latter proof system can be turned into a refutation of size ≤ p(l) in the former proof system. However, the converse does not hold: there are families of inconsistent CNF formulae over n variables for which any resolution proof of a contradiction is of size exponential in n, while when the formulae are encoded in a natural way as pseudo-Boolean constraints, cutting planes refutations of size linear in n exist. This is the case for the family of inconsistent pigeonhole instances [Haken, 1985; Krishnamurthy, 1985]. This explains why several dedicated solvers that aim to take advantage of the strength of the cutting planes system have been implemented [Barth, 1995; Dixon and Ginsberg, 2002; Chai and Kuehlmann, 2003; Sheini and Sakallah, 2006; Le Berre and Parrain, 2010].

In this paper, we do not consider issues about proof systems but instead analyse the properties of the language PBC of pseudo-Boolean constraints and those of its subset, the language CARD of cardinality constraints, concerning the representation of propositional information. In this direction, several questions have to be considered concerning the spatial efficiency of the two languages (i.e., their ability to represent propositional information using little space) as well as their temporal efficiency (i.e., the ability to exhibit a number of queries and transformations which are tractable when the information used is encoded in the language). Of specific interest are the advantages and disadvantages of PBC and CARD compared to CNF. For instance, it is known that the language CNF is not more succinct than the language FBDD of free binary decision diagrams. Does this also hold for PBC or CARD? It is also known that deciding whether a consistent conjunction of literals implies a CNF formula can be done in polynomial time. Does this still hold for PBC or CARD representations? Addressing those issues in a principled way amounts to considering the criteria used in the knowledge compilation map for comparing target compilation languages [Darwiche and Marquis, 2002]. Though neither PBC nor CARD can be considered as compilation languages (since none of them offers a polynomial-time algorithm for deciding consistency), we argue that the criteria (succinctness, polynomial-time queries and transformations) used to compare compilation languages are meaningful for other propositional languages since they provide a systematic approach to the questions above.

Thus, in the following, the relative succinctness of PBC and CARD compared to many standard propositional languages (CNF, NNF, OBDD, etc.) is determined. Then, we examine whether the queries and transformations which are considered in the knowledge compilation map are supported efficiently by PBC and CARD or not (which amounts to deciding whether a polynomial-time algorithm for carrying out the query or the transformation exists or not - unconditionally or unless P = NP). Our results show that, on the one hand, despite the extra succinctness of CARD and PBC compared to CNF, their relation to standard propositional languages like DNF, OBDD, FBDD is the same: those languages which are incomparable to CNF w.r.t. succinctness are also incomparable to PBC w.r.t. succinctness. On the other hand, the improvement w.r.t. spatial efficiency which results from such a switch does not imply the loss of many tractable queries or transformations: all the queries and all the transformations, offered by CNF except SFO and ∨BC are preserved.

2 Preliminaries

We consider a propositional setting based on a finite set of propositional variables. A literal is a variable or its negation and a clause is a disjunction of literals. All the representations considered in the following are interpreted in the classical way, so that the notions of consistency, validity, entailment, equivalence are the standard ones. |= denotes entailment and ≡ denotes equivalence. The size of a representation ϕ, denoted |ϕ|, is the number of elementary symbols used in ϕ (integers are represented in binary notation).

2.1 Pseudo-Boolean Constraints

Among all the propositional representations considered in the following we are specifically interested in pseudo-Boolean constraints.

Definition 2.1 (Pseudo-Boolean constraint). A pseudoBoolean constraint is of the form ∑ni=1 aili △ k, where n is some non-negative integer, ∀i ∈ {1, . . . , n}, ai ∈ Z, li is a literal, △ ∈ {<,≤,=,≥,>} and k ∈ Z. Each ai is called a weight and k is called the degree of the constraint.

A normalized pseudo-Boolean constraint is a pseudoBoolean constraint of the form ∑ni=1 aili ≥ k, where ∀i ∈ {1, . . . , n}, ai ∈ N, k ∈ N and each variable appears only once in the constraint, either positively or negatively. From now on, we assume that all the pseudo-Boolean constraints under consideration are normalized. This assumption is harmless, computationally speaking:

Proposition 2.2 ([Barth, 1995; Roussel and Manquinho, 2009]). Any pseudo-Boolean constraint can be turned in polynomial time into an equivalent, normalized pseudoBoolean constraint, or a conjunction of such constraints.

In the following, we also focus on a specific family of pseudo-Boolean constraints, consisting of cardinality constraints. A cardinality constraint is a normalized pseudoBoolean constraint of the form ∑ni=1 li ≥ k where n is some non-negative integer.

Definition 2.3 (PBC, CARD). PBC (resp. CARD) is the language of conjunctions of normalized pseudo-Boolean constraints (resp. cardinality constraints).

In this paper, we use the following inference rules to reason with pseudo-Boolean constraints:

• Saturation. Let κ be a (normalized) pseudo-Boolean constraint κ = ∑ni=1 aili ≥ k where for some i0 in {1, . . . , n}, ai0 > k. Then, ai0 can be replaced by k without changing the models of the constraint.
• Division. Let κ be a (normalized) pseudo-Boolean constraint κ = ∑ni=1 aili ≥ k and an integer α > 0. κ entails the constraint ∑ni=1 ⌈ ai α ⌉li ≥ ⌈ kα ⌉, where ⌈x⌉ denotes the smallest integer greater or equal to x. Moreover, if α is a divisor of each ai, then κ is equivalent to the latter constraint.

Note that, in the division rule, we do not require k to be divisible by α. This property allows the proof system to be more powerful than resolution [Cook et al., 1987]. For example, the constraint 2x+2y +2z ≥ 3 becomes x+y +z ≥ 2, which eliminates some non-integral solutions.

2.2 Knowledge CompilationMap

The knowledge compilation map reported in [Darwiche and Marquis, 2002] is a systematic, multi-criteria comparative analysis of propositional representation languages. The choice of a language L is then guided by its spatial efficiency (its succinctness) and its temporal efficiency (the queries and transformations it offers, viewed as properties of L).

Succinctness. Succinctness captures the (relative) ability of a language to represent information using little space, and yields a pre-order ≤s. A propositional language L1 is said to be at least as succinct as another language L2, denoted L1 ≤s L2, if and only if there exists a polynomial p such that for every formula α ∈ L2, there exists an equivalent formula β ∈ L1 where |β| ≤ p(|α|). When L1 ≤s L2 and L2 ̸≤s L1, we write L1 <s L2.

Queries. A query takes as input one or more representations from L, and some other inputs can be also required, such as clauses, terms, etc. It typically returns a Boolean value or a number. A language L satisfies a given query when a polynomial-time algorithm exists for answering the query, i.e., returning the expected result.

For example, let us consider clausal entailment, a query which returns a Boolean value stating whether or not a given clause is entailed by a representation from L:

Definition 2.4 (CE). L satisfies CE (Clausal Entailment) if and only if there exists a polynomial-time algorithm that decides whether ϕ |= γ where ϕ ∈ L and γ is a clause.

Other queries, such as CO (consistency), VA (validity), IM (implication by a term), EQ (equivalence), SE (sentential entailment), CT (model counting) and ME (model enumeration), that have been considered in the knowledge compilation map, are also taken into account in the following. For space reasons, the reader is referred to [Darwiche and Marquis, 2002] for some formal definitions.

Transformations. A transformation takes as input one or more representations from L, and some other inputs can be also required, such as variables, terms, etc. The result is a representation from L.

For example, let us consider the closures under ∧ and ∨:

Definition 2.5 (∧C, ∨C). L satisfies ∧C (resp. ∨C) if and only if there exists a polynomial-time algorithm which computes a representation from L that is equivalent to ϕ1 ∧ · · · ∧ ϕn (resp. ϕ1 ∨ · · · ∨ ϕn) given a set of formulae ϕ1, . . . , ϕn from L as input.

The other transformations considered in the knowledge compilation map, namely CD (conditioning), FO (forgetting), SFO (singleton forgetting), ∧BC (bounded closure under ∧), ∨BC (bounded closure under ∨) and ¬C (closure under ¬), are also considered in the following. Again, formal definitions can be found in [Darwiche and Marquis, 2002].

3 Succinctness of Pseudo-Boolean Constraints

In this section, PBC and CARD are compared in terms of succinctness with many languages considered in the knowledge compilation map, namely NNF, CNF, DNF, IP, DNNF, FBDD, OBDD, OBDD<, and MODS. Special attention is devoted to the language of (DAG-based) Negation Normal Form representations (NNF) [Darwiche, 1999; 2001], the language of Ordered Binary Decision Diagram (OBDD<) [Bryant, 1986], and the language of Prime Implicants (IP) [Quine, 1952] since all the new succinctness results which have been identified actually are by-products of the succinctness results involving PBC, CARD and those three languages. The results obtained are summarized by the diagram in Figure 1.

Let us now detail the claimed results:

Proposition 3.1. PBC <s CARD.

Proof. First, since CARD is a subset of PBC, we get that PBC ≤s CARD.

Now, let us prove that CARD ̸≤s PBC. Let κ be the pseudo-Boolean constraint defined by κ = kx + ∑2k i=1 xi ≥ k. Let κ′ = ∑mi=1 li ≥ k′ be a non-valid pseudo-Boolean constraint such that κ |= κ′ , and Var(κ′ ) ⊆ Var(κ). We first show that, necessarily, k′ = 1, i.e., κ′ is a clause.

Let us suppose that k′ > 1, and let us consider M the model of κ such that x is satisfied, and any literal which is in κ′ is falsified, except x. In this interpretation, we necessarily have ∑mi=1 li ≤ 1, since only x is satisfied by construction. Indeed, if x positively appears in κ′ , then ∑mi=1 li = 1. Otherwise, ∑mi=1 li = 0. In both cases, since we have assumed k′ > 1, κ′ is not satisfied, so M is not a model of κ′ . This contradicts that κ |= κ′ , so k′ ≤ 1. Since κ′ is supposed to be non-valid, k′ cannot be equal to 0, so k′ = 1.

The only way to represent κ as a conjunction of cardinality constraints is then to use clauses, since all these constraints must be implied by κ. However, thanks to Proposition 4.1.4 from [Dixon, 2004], we have that an exponential number of clauses is required to represent κ, and this completes the proof.

Proposition 3.2. NNF ≤s PBC.

Sketch of Proof. Let κ = ∑ni=1 aili ≥ k be a pseudoBoolean constraint. It is well known that any pseudo-Boolean constraint ∑ni=1 aili ≥ k can be represented by an equivalent NNF representation of polynomial size (see e.g. [Vollmer, 1999]). Now, when a conjunction of pseudo-Boolean constraints is considered, an NNF representation of it consists of the conjunction of all these "elementary" NNF representations - one per pseudo-Boolean constraint.

As an immediate consequence of [Dixon, 2004] (Proposition 4.1.4), we have the following result:

Proposition 3.3. CARD <s CNF

Let us now show that PBC is not at least as succinct as OBDD<.

Proposition 3.4. PBC ̸≤s OBDD<

Proof. Let ϕ = ⊕nj=1 xj. ϕ is true if and only if there is an odd number of satisfied xj .

This formula can be written as an OBDD< representation of polynomial size [Bryant, 1986]. Let us prove that every representation of ϕ as a conjunction of pseudo-Boolean constraints requires an exponential number of constraints.

Let κ = ∑mi=1 aili ≥ k be a non-valid pseudo-Boolean constraint, such that ϕ |= κ, with Var(κ) ⊆ Var(ϕ). Let us note L+ and L- the sets of positive and negative literals of κ, respectively.

Claim 3.5. We have Var(κ) = Var(ϕ).

Sketch of Proof. If there is x ∈ Var(ϕ) such that x ̸∈ Var(κ), then any counter-model of κ can be turned into a model M of ϕ by keeping the same assignment, except for x, which must be satisfied. M is still a counter-model of κ, which contradicts ϕ |= κ.

Claim 3.6. |L-| is even.

Proof. Let us suppose that |L-| is odd. Let M be the interpretation given by M = {xj|xj ∈ L-}. M satisfies an odd number of xj , so it is a model of ϕ. However, M does not satisfy any literal of κ, so it is not a model of κ. This contradicts ϕ |= κ, so |L-| is even.

Claim 3.7. We have ∀i ∈ {1, . . . ,m}, ai = k.

Proof. With the saturation rule, one can ensure that ai ≤ k for all i ∈ {1, . . . ,m}. Let us assume that ∃i0 ∈ {1, . . . ,m}, ai0 < k and that the variable associated with li0 is xj0 . There are two possible cases: xj0 ∈ L+ or xj0 ∈ L-. In the case when xj0 ∈ L+, let us consider the interpretation given by M = {xj0 } ∪ {xj |xj ∈ L-}. By Claim 3.6, since |L-| is even, |M| = |L-| +1 is odd, and M is a model of ϕ. In the remaining case, xj0 ∈ L-, and then let us consider the interpretation given by M = {xj|xj ∈ L-}\{xj0 }. Since |L-| is even, |M| = |L-| -1 is odd, and M is a model of ϕ. In both cases, ∑mi=1 aili = ai0 < k, so M is not a model of κ. This contradicts ϕ |= κ, so ∀i ∈ {1, . . . ,m}, ai = k.

So, κ = ∑mi=1 kli ≥ k, and the division rule gives us that κ ≡ ∑mi=1 li ≥ 1, i.e., κ is equivalent to clause. Then, the only way to represent ϕ as a conjunction of pseudo-Boolean constraints is to use clauses, since all these constraints must be implied by ϕ. Since ϕ requires an exponential number of clauses to be represented without introducing new variables - all the clauses contain all the variables by Claim 3.5 - the claim follows.

Proposition 3.8. PBC ̸≤s IP

Proof. Let ϕ = ∨nj=1 (xj ∧ yj) be a formula from IP [Darwiche and Marquis, 2002]. We now show that representing ϕ as a conjunction of pseudo-Boolean constraints requires an exponential number of constraints.

Let κ = ∑mi=1 aili ≥ k be a pseudo-Boolean constraint such that ϕ |= κ, with Var(κ) ⊆ Var(ϕ) and k > 0.

Claim 3.9. For all j ∈ {1, . . . , n}, xj or yj appears positively in κ.

Sketch of Proof. If neither xj nor yj appear in Var(κ), then the model of ϕ satisfying xj and yj but falsifying all the literals of κ is not a model of κ, which contradicts ϕ |= κ.

Claim 3.10. For all j ∈ {1, . . . , n}, if xj appears positively in κ, and yj does not, then the weight of xj is k. Symmetrically, for all j ∈ {1, . . . , n}, if yj appears positively in κ, and xj does not, then the weight of yj is k.

Sketch of Proof. If only xj appears positively in κ, say xj = lj0 , and aj0 < k, then the model of ϕ satisfying both xj and yj but falsifying all the other literals of κ is not a model of κ, which contradicts ϕ |= κ. The proof for the case when only yj appears positively in κ is similar.

Claim 3.11. For all j ∈ {1, . . . , n}, if xj and yj appear positively in κ, then the sum of their weights is at least equal to k.

Sketch of Proof. If both xj and yj appear positively as lj0 and lj1 in κ, respectively, and aj0 +aj1 < k, then the model of ϕ satisfying these two literals but falsifying all the others of κ is not a model of κ, which contradicts ϕ |= κ.

Claim 3.12. Without loss of generality, κ can contain only positive literals.

Sketch of Proof. If yj appears in κ, let κ′ be the pseudoBoolean constraint obtained by removing the literal yj from κ. The case where xj appears in κ follows symmetrically.

Any model M of ϕ is a model of κ′ . Indeed, if M satisfies yj, then it is obviously a model of κ′ . Otherwise, there exists i ̸= j such that M satisfies xi and yi, and by Claims 3.9, 3.10 and 3.11, κ′ is also satisfied byM.

So, ϕ |= κ′ , and since we obviously have that κ′ |= κ, it is possible to replace κ by κ′ without losing information. All negative literals can be removed by repeating the same argument.

Let K = ∧mj=1 κj be any conjunction of pseudo-Boolean constraints such that ϕ ≡ K. Thanks to the previous results, we have: ∀j ∈ {1, . . . ,m}, κj = ∑ni=1 a0,i,jxi + a1,i,jyi ≥ kj, with, ∀i ∈ {1, . . . , n}, a0,i,j + a1,i,j ≥ kj by applying Claim 3.11.

Any counter-model of ϕ must be a counter-model of K. It remains to show, in the rest of this proof, that a subset of these counter-models requires the use of an exponential number of pseudo-Boolean constraints to get a formula logically equivalent to ϕ.

Any interpretation satisfying for all i ∈ {1, . . . , n} exactly one of xi or yi cannot be a model of K, since it is not a model of ϕ. Then, it must not satisfy at least one of the constraints

κj. Formally, this means that the following property must be satisfied.

For each of the inequalities induced by (∗), we define a tuple (f(1), . . . , f(n)) ∈ Bn . We claim that two inequalities associated with such tuples which have a Hamming distance at least equal to 2 cannot be satisfied for a same j. Otherwise, let (f1(1), . . . , f1(n)) and (f2(1), . . . , f2(n)) be two tuples with a Hamming distance at least equal to 2 for a same j. Their associated inequalities are (1) ∑ni=1 af1(i),i,j < kj and (2) ∑ni=1 af2(i),i,j < kj. Since the Hamming distance between the two tuples is at least equal to 2, there exists α, β ∈ {1, . . . , n}, with α ̸= β, such that f1(α) ̸= f2(α) and f1(β) ̸= f2(β). By adding (1) and (2), since f1 and f2 take their values in {0, 1}, we get:

However, this is impossible since Claim 3.11 gives us a0,α,j + a1,α,j ≥ kj and a0,β,j + a1,β,j ≥ kj, so a0,α,j + a1,α,j + a0,β,j + a1,β,j ≥ 2kj . So, we need two distinct constraints to satisfy the inequalities of (∗) associated with these tuples.

Claim 3.13. There exists a set of 2n-1 tuples of Bn having pairwise Hamming distance at least 2.

Sketch of Proof. Consider the set S of solutions over {0, 1} of ∑ni=1 zi is equivalent to 0 mod 2. The elements of S have pairwise Hamming distance at least 2. Finally, S contains 2n-1 elements since any assignment to z1, . . . , zn-1 can be extended to a solution in S.

Hence, to get satisfied, the system of inequalities associated with these tuples requires at least 2n-1 distinct constraints. So, representing ϕ as a conjunction of pseudo-Boolean constraints requires exponentially many constraints.

The remaining succinctness results reported in Figure 1 are easy consequences of the previous one, taking advantage of the transitivity of ≤s and of the succinctness results given in [Darwiche and Marquis, 2002; Bova et al., 2016].

4 Querying Pseudo-Boolean Constraints

We now present the results about the queries offered by PBC and CARD summarized in Table 1.

Proposition 4.1. CARD does not satisfy CO, CE, EQ, SE, CT and ME, unless P = NP.

Proof. Since the translation of any CNF formula into a conjunction of cardinality constraints can be done in polynomial time, and since CNF does not satisfy any of these properties, unless P = NP, the claim follows.

Since CARD is a sublanguage of PBC, we get:

Corollary 4.2. PBC does not satisfy CO, CE, EQ, SE, CT and ME, unless P = NP.

We also have that:

Proposition 4.3. PBC and CARD satisfy VA.

Proof. A conjunction of pseudo-Boolean constraints is valid if and only if all of its constraints are valid. This is the case if and only if all the constraints have a degree equal to 0, which can be checked in polynomial time.

Since PBC and CARD satisfy VA and CD (cf. Section 5), the following corollary follows immediately by Lemma A.7 from [Darwiche and Marquis, 2002].

Corollary 4.4. PBC and CARD satisfy IM.

5 Transforming Pseudo-Boolean Constraints

Finally, we present the results we have obtained about the transformations offered by PBC and CARD. They are summarized in Table 2.

Proposition 5.1. PBC and CARD satisfy CD.

Proof. Computing the conditioning of any formula from PBC (resp. CARD) is easily done by replacing, in each constraint, every literal of the conditioning term by a Boolean constant. This produces, after a trivial normalization step made in polynomial time, a conjunction of pseudo-Boolean constraints (resp. cardinality constraints).

Proposition 5.2. CARD and PBC satisfy both ∧BC and ∧C.

Proof. Given a conjunctively-interpreted set of formulae from CARD (resp. PBC), computing the conjunction of these formulae can trivially be done in polynomial time.

Proposition 5.3. CARD does not satisfy ∨BC.

Proof. Let ϕ be the disjunction of the two cardinality constraints κ = y ≥ 1 (κ ≡ y) and κ′ = ∑2n i=1 xi ≥ n. It is easy to see that ϕ is equivalent to ny + ∑2n i=1 xi ≥ n. As shown in the proof of Proposition 3.1, a representation of this constraint using only cardinality constraints requires exponentially many constraints. Hence, the claim follows.

Proposition 5.4. PBC does not satisfy ∨BC.

Proof. To prove this result, we show that any representation of the inequality ∆ = ∑2n i=1 xi ̸= n, which is equivalent to the disjunction of ∑2n i=1 xi ≥ n+1 and ∑2n i=1 xi ≥ n+1, requires an exponential number of pseudo-Boolean constraints when n ≥ 2.

Let us consider a non-valid pseudo-Boolean constraint κ = ∑mi=1 aili ≥ k, such that ∆ |= κ, with Var(κ) ⊆ Var(∆). Let us note L+ and L- the sets of positive and negative literals of κ, respectively.

Sketch of Proof. Consider I a counter-model of κ. Since ∆ |= κ, I satisfies n of the xi. If x in Var(∆) but x ̸∈ Var(κ), then the interpretation I ′ defined by I ′ = I ∪ {x} satisfies n + 1 of the xi, so it is a model of ∆, but not a model of κ, which contradicts ∆ |= κ.

Claim 5.6. We have |L+| = |L-|.

Proof. If |L+| < |L-|, then by Claim 5.5, we necessarily have |L-| > n. The interpretation M = {xi|xi ∈ L-} satisfies strictly more than n of the xi, so it is a model of ∆, but not a model of κ. If |L-| < |L+|, then by Claim 5.5, we necessarily have |L+| > n. The interpretation M = {xi|xi ∈ L-} satisfies strictly less than n of the xi, so it is a model of ∆, but not a model of κ. In both cases, ∆ |= κ is contradicted, so |L+| = |L-|.

Claim 5.7. We have ∀i ∈ {1, . . . ,m}, ai = k.

Proof. Let us suppose that ∃i0 ∈ {1, . . . ,m}, ai0 < k and that the variable associated with li0 is xi′0 .

There are two possible cases: either xi′0 ∈ L+ or xi′0 ∈ L-. If xi′0 ∈ L+, let us consider the interpretation M = {xi′0 } ∪ {xi|xi ∈ L-}. Then, by Claims 5.5 and 5.6, M satisfies n + 1 of the xi, so it is a model of ∆. Otherwise, xi′0 ∈ L- and let us consider the interpretation M = {xi|xi ∈ L-}\{xi′0 }. Then, M satisfies (n-1) of the xi, so it is a model of ∆. In both cases, ∑ni=1 aili = ai′0 < k, so M is not a model of κ. ∆ |= κ is contradicted, so ∀i ∈ {1, . . . ,m}, ai = k.

Thus, the division rule gives that κ = ∑mi=1 kli ≥ k ≡ ∑mi=1 li ≥ 1, in other words, κ is equivalent to a clause. The only way to represent ∆ as a conjunction of pseudo-Boolean constraints is then to use clauses, since all the constraints must be implied by ∆.

However, ∆ requires an exponential number of clauses to be represented without introducing any new variable. Indeed, a clause as the ones we have produced in this proof can only eliminate a single counter-model of ∆, since all those clauses contain all the variables, and there exist (2n n ) counter-models. Hence, the claim follows.

We also have that:

Proposition 5.9. PBC does not satisfy SFO.

Proof. Let κ and κ′ be the two pseudo-Boolean constraints defined by ∑2n i=1 xi ≥ n + 1 and ∑2n i=1 xi ≥ n + 1, respectively. Let us consider, for s a newly introduced variable, the formulae κs = (n + 1)s + ∑2n i=1 xi ≥ n + 1 and κ′s = (n + 1)s + ∑2n i=1 xi ≥ n + 1, which are obtained from κ and κ′ in polynomial time.

Let ϕ = κs ∧ κ′s . By construction, ϕ|s ≡ κ′ and ϕ|¯ s ≡ κ. So, ∃xϕ ≡ κ ∨ κ′ . If an algorithm existed to forget a single variable in a set of pseudo-Boolean constraints, then one could use it to compute in polynomial time the disjunction of κ and κ′ . However, we have proven that it is not possible (cf. Proposition 5.4). Then, so it is for the forgetting of a single variable in a conjunction of pseudo-Boolean constraints.

Corollary 5.10. PBC does not satisfy FO.

We also have that:

Proposition 5.11. CARD does not satisfy FO, unless P = NP.

Proof. As for CNF, if CARD satisfied FO, then it would be possible to compute CO on a formula from CARD in polynomial time. Indeed, a formula is consistent precisely when the representation obtained by forgetting all its variables in it evaluates to true (which can be tested easily since the set of variables of the resulting formula is empty).

6 Conclusion

We have studied the language PBC of pseudo-Boolean constraints and the language CARD of cardinality constraints from a knowledge representation perspective. Our results show that switching from CNF to CARD and then to PBC increases the succinctness of the representations but does not lead to languages that would be at least as succinct as other propositional languages, like DNF, OBDD, or FBDD. Interestingly, such a switch does not lead to the loss of any tractable query that is supported by CNF. As to the transformations, both PBC and CARD lose ∨BC, and PBC loses SFO as well. No transformation is gained w.r.t. CNF.

Accordingly, when dealing with applications involving propositional representations but not requiring to perform any transformation among SFO and ∨BC, we now know that the languages PBC and CARD are valuable alternatives to CNF due to the succinctness increase they may lead to. Of course, every PBC representation Σ can be turned in linear time into a CNF representation Φ which is not equivalent to it, but has the same logical consequences over the variables occurring in Σ. The translations used to go from Σ to Φ (especially those reported in [Plaisted and Greenbaum, 1986; Tseitin, 1968]) consist in introducing in Φ additional variables not occurring in Σ (in fact, Σ is equivalent to the formula we get by forgetting those variables in Φ). Since such translations can be achieved in linear time, the size of Φ is also linear in that of Σ. While using Φ instead of Σ is a feasible alternative for answering certain queries over the variables occurring in Σ, it must be noted that Φ cannot be substituted to Σ in every setting, i.e., for answering any query or achieving any transformation. For instance, Φ and Σ do not have the same implicants in the general case. In addition the queries and transformations offered by the language of CNF with some existentially quantified variables (alias the existential closure of CNF) do not coincide with those offered by PBC and CARD [Fargier and Marquis, 2008]. All this explains why the extra succinctness of PBC and CARD compared to CNF can be considered as a decisive advantage for some applications.

Acknowledgements

The authors are grateful to the anonymous reviewers for their numerous comments. These comments greatly helped to improve the presentation of the paper. Part of this work was supported by the French Ministry for Higher Education and Research, the Hauts-de-France Regional Council through the "Contrat de Plan ´Etat R´egion (CPER) DATA" and an EC FEDER grant.