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

as

where we are now thinking of and as variables with value either 0 (false) or 1 (true) and have written for or, equivalently, . If is a variable, we will continue to refer to as the negation of .

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

with

to get , we simply add

to

and simplify using the identity to get

as required.

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

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

**Proof.** Cook et al. Cook:php give a derivation in
steps; we have presented an derivation elsewhere
[Dixon GinsbergDixon Ginsberg2000].

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:

is logically equivalent to the set of axioms

for every set of distinct variables . 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 of variables. Suppose also
that is the set of 's that are true, so that is of size
at least . Since there are only variables,
and at least one must be true.

To see that (20) implies (19), suppose that (20) is true for all appropriate sets of 's. Now if (19) were false, the set of false 's would be of size at least , 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

then it must also imply

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

Next, note that no axiom of length less than 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 of (20) but include all of the others as well as every clause of length greater than . By setting the variables in 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 instances of (20).

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:

where each and is a positive integer and each of the 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 are the weights
attached to various literals. The pseudo-Boolean language is somewhat more
flexible still, allowing us to say (for example)

indicating that either is true or both and 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.

- Unit Propagation

- Inference and Resolution
- Learning and Relevance Bounds

- Proof Complexity
- Modularity constraints and pseudo-Boolean encodings
- Pseudo-Boolean constraints and extended resolution

- Summary