   Next: Subsearch and quantification Up: Unit Propagation Previous: Unit Propagation

### Subsearch

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:

1. In Procedure 2.2 (DPLL) (and similarly in WSAT), we need to determine if is a solution to the problem at hand. This involves searching for an unsatisfied clause.
2. In Procedure 2.3 (unit propagation), we need to find unsatisfied clauses that contain at most one unvalued literal.
In addition, WSAT needs to compute the number of clauses that will become unsatisfied when a particular variable is flipped.

All of these tasks can be rewritten using the following:

Definition 5.1   Suppose is a set of quantified clauses, and is a partial assignment of values to the atoms in those clauses. We will denote by the set of ground instances of that have literals unvalued by and literals satisfied by the assignments in .15

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.

Proposition 5.2   For fixed and , the checking problem is NP-complete.

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 (43)

as in Definition 3.4 we allow axioms such as (replacing the inequality in (43) with an equality), determining whether a single axiom is satisfiable becomes weakly NP-complete. Symmetry, the other example we have examined, involves no effective change in the representational power of a single axiom.

Here is a recasting of unit propagation in terms of Definition 5.1:

Procedure 5.3 (Unit propagation)   To compute : It is important to recognize that this recasting is not changing the procedure in any significant way; it is simply making explicit the subsearch tasks that were previously described only implicitly. The procedure itself is unchanged, and other procedural details such as variable and value choice heuristics are irrelevant to the general point that unit propagation depends on solving a subsearch instance at every step. WSAT is similar.   Next: Subsearch and quantification Up: Unit Propagation Previous: Unit Propagation
Matt Ginsberg 2004-02-19