Next: Unit Propagation Up: Generalizing Boolean Satisfiability I: Previous: Boolean Summary

# 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
 (18)

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:

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

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

The cardinality constraint simply says that at least 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 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:

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

is logically equivalent to the set of axioms
 (20)

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:

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

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.

Subsections

Next: Unit Propagation Up: Generalizing Boolean Satisfiability I: Previous: Boolean Summary
Matt Ginsberg 2004-02-19