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
All of the familiar logical operations have obvious analogs in this
notation. If, for example, we want to resolve
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:
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:
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
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:
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)