Pseudo-Boolean and Cardinality Constraints

The entries in the previous table summarize the fact that Boolean satisfiability is a weak method that admits efficient implementations. The representation is relatively inefficient, and none of our canonical problems can be solved in polynomial time. Some of these difficulties, at least, can be overcome via a representational shift.

To understand the shift, note that we can write an axiom such as

$$x \vee y \vee \neg z$$

as

$$x+y+\overline z \geq 1$$ (18)

where we are now thinking of $x,y$ and $z$ as variables with value either 0 (false) or 1 (true) and have written $\overline z$ for $1-z$ or, equivalently, $\neg z$. If $v$ is a variable, we will continue to refer to $\overline v$ as the negation of $v$.

All of the familiar logical operations have obvious analogs in this notation. If, for example, we want to resolve

$$a \vee \neg b \vee c$$

with

$$b \vee \neg d$$

to get $a\vee c \vee \neg d$, we simply add

$$a+\overline b+c \geq 1$$

to

$$b+\overline d \geq 1$$

and simplify using the identity $b+\overline b=1$ to get

$$a+c+\overline d \geq 1$$

as required.

What's nice about this notation is that it extends easily to more general descriptions. If the general form of a disjunction $\vee l_i$ of literals is $\sum l_i \geq 1$ as in (18), we can drop the requirement that the right-hand side be 1:

Definition 3.1   A cardinality constraint or extended clause is a constraint of the form

$$\sum_i l_i \geq k$$

where $k$ is an integer and each of the $l_i$ is required to have value 0 or 1.

The cardinality constraint simply says that at least $k$ of the literals in question are true.

Proposition 3.2 (Cook, Coullard and Turan Cook:php)   There is an unsatisfiability proof of polynomial length of the pigeonhole problem using cardinality constraints.

Proof. Cook et al. Cook:php give a derivation in $o(n^3)$ steps; we have presented an $o(n^2)$ derivation elsewhere [Dixon GinsbergDixon Ginsberg2000].         $\mathchoice{\vcenter{\hrule height.4pt \hbox{\vrule width.4pt height3pt \kern ... ...vrule width.3pt height1.5pt \kern 1.5pt \vrule width.3pt} \hrule height.3pt}}$

Of course, the fact that this extension to the SAT language allows us to find polynomial-length derivations of pigeonhole problem does not necessarily show that the change will have computational value; we need to examine the other columns of the table as well. In the remainder of this section, we will show this and will go further, describing new computational techniques that can only be applied in the broader setting that we are now considering. Experimental results are also presented. But let us begin by examining the first column of the table:

Proposition 3.3   [Benhamou, Sais, SiegelBenhamou et al.1994] The cardinality constraint

$$x_1 + \cdots + x_m \geq k$$ (19)

is logically equivalent to the set of $m \choose {k-1}$ axioms

$$x_{i_1} + \cdots + x_{i_{m-k+1}} \geq 1$$ (20)

for every set of $m-k+1$ distinct variables $\{x_{i_1},\dots,x_{i_{m-k+1}}\}$. Furthermore, there is no more compact Boolean encoding of (19).

Proof. We first show that (19) implies (20). To see this, suppose that we have a set $S$ of $m-k+1$ variables. Suppose also that $T$ is the set of $x_i$'s that are true, so that $T$ is of size at least $k$. Since there are only $m$ variables, $S\cap T \neq {\hbox{\rm\O}}$ and at least one $x_i\in S$ must be true.

To see that (20) implies (19), suppose that (20) is true for all appropriate sets of $x_i$'s. Now if (19) were false, the set of false $x_i$'s would be of size at least $m-k+1$, so that some instance of (20) would be unsatisfied.

To see that there is no more efficient encoding, first note that if (19) implies a Boolean axiom

$$x_1\vee\cdots\vee x_k\vee \neg x_{k+1}\vee\cdots\vee \neg x_m$$

then it must also imply

$$x_1\vee\cdots\vee x_k$$

since we can always change an $x_i$ from false to true without reducing the satisfiability of (19).

Next, note that no axiom of length less than $m-k+1$ is a consequence of (19), since any such axiom can be falsified while satisfying (19) by setting every unmentioned variable to true and the rest to false.

Finally, suppose that we leave out a single instance $i$ of (20) but include all of the others as well as every clause of length greater than $m-k+1$. By setting the variables in $i$ to false and every other variable to true, all of the given clauses will be satisfied but (19) will not be. It follows that any Boolean equivalent of (19) must include at least the $m \choose {k-1}$ instances of (20).         $\mathchoice{\vcenter{\hrule height.4pt \hbox{\vrule width.4pt height3pt \kern ... ...vrule width.3pt height1.5pt \kern 1.5pt \vrule width.3pt} \hrule height.3pt}}$

It follows from Proposition 3.3 that provided that no new variables are introduced, cardinality constraints can be exponentially more efficient than their Boolean counterparts.

Before discussing the other columns in the table, let us consider further extending our representation to include what are known as pseudo-Boolean constraints:

Definition 3.4   A pseudo-Boolean constraint is an axiom of the form

$$\sum_i w_i l_i \geq k$$ (21)

where each $w_i$ and $k$ is a positive integer and each of the $l_i$ is required to have value 0 or 1.

Pseudo-Boolean representations typically allow both linear inequalities and linear equalities over Boolean variables. Linear equalities can easily be translated into a pair of inequalities of the form in the definition; we prefer the inequality-based description [BarthBarth1996,Chandru HookerChandru Hooker1999, also known as pseudo-Boolean normal form] because of the better analogy with Boolean satisfiability and because unit propagation becomes unmanageable if equality constraints are considered. Indeed, simply determining if an equality clause is satisfiable subsumes subset-sum and is therefore (weakly) NP-complete [Garey JohnsonGarey Johnson1979].

Compare (21) with Definition 3.1; the $w_i$ are the weights attached to various literals. The pseudo-Boolean language is somewhat more flexible still, allowing us to say (for example)

$$2a + b + \overline c \geq 2$$

indicating that either $a$ is true or both $b$ and $\neg c$ are (equivalent to the crucial representational efficiency obtained in extended resolution). As we will see shortly, it is natural to make this further extension because the result of resolving two cardinality constraints can be most naturally written in this form.