Our primary goal here is to work with the quantified formulation
directly, as opposed to its much larger ground translation.
Unfortunately, there are significant constant-factor costs incurred in
doing so, since each inference step will need to deal with issues
involving the bindings of the variables in question. Simply finding
the value assigned to 
might well take several times longer
than finding the value assigned to the equivalent 
. Finding
all occurrences of a given literal can be achieved in the ground case
by simple indexing schemes, whereas in the quantified case this is
likely to require a unification step. While unification can be
performed in time linear in the length of the terms being unified, it
is obviously not as efficient as a simple equality check. Such
routine but essential operations can be expected to significantly slow
the cost of every inference undertaken by the system.
Our fundamental point here is that while there are costs associated with using quantified axioms, there are significant savings as well. These savings are a consequence of the fact that the basic unit propagation procedure uses an amount of time that scales roughly linearly with the size of the theory; use of quantified axioms can reduce the size of the theory so substantially that the constant-factor costs can be overcome.
We will make this argument in two phases. In Section 5.1.1, we generalize a specific computational subtask that is shared by unit propagation and other satisfiability procedures such as WSAT. We will show this generalization to be NP-complete in a formal sense, and we call it subsearch for that reason. The specific procedures for unit propagation and as needed by WSAT encounter this NP-complete subproblem at each inference step, and we show that while subsearch is generally not a problem for randomly generated theories, the subsearch cost can be expected to dominate the running time on more realistic instances.
In Section 5.1.2, we discuss other consequences of the fact that subsearch is NP-complete. Search techniques can be used to speed the solution of NP-complete problems, and subsearch is no exception. We show that quantified axiomatizations support the application of simple search techniques to the subsearch problem, and argue that realistic examples are likely to lead to subsearch problems of only polynomial difficulty although existing unit propagation implementations solve them exponentially.