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 $P$ 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 $C$ is a set of quantified clauses, and $P$ is a partial assignment of values to the atoms in those clauses. We will denote by $S_u^s(C,P)$ the set of ground instances of $C$ that have $u$ literals unvalued by $P$ and $s$ literals satisfied by the assignments in $P$.¹⁵

We will say that the checking problem is that of determining whether $S_u^s(C,P) \neq {\hbox{\rm\O}}$. By a subsearch problem, we will mean an instance of the checking problem, or the problem of either enumerating $S_u^s(C,P)$ or determining its size.

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

Proof. Checking is in NP, since a witness that $S_u^s(C,P) \neq {\hbox{\rm\O}}$ need simply give suitable bindings for the variables in each clause of $C$.

To see NP-hardness, we assume $u=s=0$; other cases are not significantly different. We reduce from a binary constraint satisfaction problem (CSP), producing a single clause $C$ and set of bindings $P$ such that $S_0^0(C,P) \neq {\hbox{\rm\O}}$ 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 $C$.

Suppose that we have a binary CSP $\Sigma$ with variables $v_1,\ldots,v_n$ and with $m$ binary constraints of the form $(v_{i1},v_{i2}) \in c_i$, where $(v_{i1},v_{i2})$ is the pair of variables constrained by $c_i$. For each such constraint, we introduce a corresponding binary relation $r_i(v_{i1},v_{i2})$, and take $C$ to be the single quantified clause $\forall v_1,\ldots,v_n. \vee_i r_i(v_{i1},v_{i2})$. For the assignment $P$, we set $r_i(v_{i1},v_{i2})$ to false for all $(v_{i1},v_{i2}) \in c_i$, and to true otherwise.

Now note that since $P$ values every instance of every $r_i$, $S_0^0(C,P)$ will be nonempty if and only if there is a set of values for $v_i$ such that every literal in $\vee_i r_i(v_{i_1},v_{i_2})$ is false. Since a literal $r_i(v_{i_1},v_{i_2})$ is false just in the case the original constraint $c_i$ is satisfied, it follows that $S_0^0(C,P) \neq {\hbox{\rm\O}}$ if and only if the original CSP $\Sigma$ was satisfiable.         $\mathchoice{\vcenter{\hrule height.4pt \hbox{\vrule width.4pt height3pt \kern ... ...vrule width.3pt height1.5pt \kern 1.5pt \vrule width.3pt} \hrule height.3pt}}$

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

$$\sum_i w_i l_i \geq k$$ (43)

as in Definition 3.4 we allow axioms such as

$$\sum_i w_i l_i = k$$

(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 $Procedure~\ref{p.Unit-Propagate}(P)$:

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.