Each iteration of DPLL (or WSAT) involves a search through the original theory for clauses that satisfy some numeric property. The specific examples that we have already seen of this are the following:
All of these tasks can be rewritten using the following:
We will say that the checking problem is that of determining whether . By a subsearch problem, we will mean an instance of the checking problem, or the problem of either enumerating or determining its size.
Proof. Checking is in NP, since a witness that need simply give suitable bindings for the variables in each clause of .
To see NP-hardness, we assume ; other cases are not significantly different. We reduce from a binary constraint satisfaction problem (CSP), producing a single clause and set of bindings such that if and only if the original binary CSP was satisfiable. The basic idea is that each variable in the constraint problem will become a quantified variable in .
Suppose that we have a binary CSP with variables and with binary constraints of the form , where is the pair of variables constrained by . For each such constraint, we introduce a corresponding binary relation , and take to be the single quantified clause . For the assignment , we set to false for all , and to true otherwise.
Now note that since values every instance of every , will be nonempty if and only if there is a set of values for such that every literal in is false. Since a literal is false just in the case the original constraint is satisfied, it follows that if and only if the original CSP was satisfiable.
Before moving on, let us place this result in context. First, and most important, note that the fact that the checking problem is NP-complete does not imply that QPROP is an unwieldy representation; the subsearch problem does indeed appear to be exponential in the size of the QPROP axioms, but there are exponentially fewer of them than in the ground case. So, as for similar results elsewhere [Galperin WigdersonGalperin Wigderson1983,PapadimitriouPapadimitriou1994], there is no net effect on complexity.
Second, the result embodied in Proposition 5.2 appears to be a general
phenomenon in that propagation is more difficult for more compact
representations. Our earlier discussion of cardinality and pseudo-Boolean axioms, for which the complexity of unit propagation was unchanged from the
Boolean case, appears to be much more the exception than the rule. As
we have already remarked, if we extend the pseudo-Boolean representation only
slightly, so that in addition to axioms of the form
Here is a recasting of unit propagation in terms of Definition 5.1: