Satisfiability algorithms have too often been developed against the framework provided by either random instances or, worse still, instances that have been designed solely to show that the technique being proposed has computational merit. The algorithms themselves have thus tended to ignore problem features that dominate the computational requirements when they are applied to real problems.
On such realistic problems, it is possible to both improve the speed
of the algorithms' inner loops (via QPROP and subsearch) and to
reduce the number of times that the inner loops need to be executed
(via learning and a move up the 
-simulation hierarchy). Both of
these classes of improvements arise because the problems in question
have structure. The structure can be learned as nogoods, or
used to re-represent the problem using pseudo-Boolean or quantified expressions.
It is true that the table in the previous subsection can be viewed as a survey of recent work on satisfiability, and it is also true that the table can be viewed as a rational reconstruction of the goals of the researchers who have investigated various representational extensions. But to our mind, the table is more accurately viewed as a report on the extent to which these linguistic or semantic modifications successfully capture problem structure.
Every column in the table is about structure. Improved representational efficiency is only possible if the problem itself has structure that a Boolean axiomatization typically obscures. It is structure that allows progress to be made in terms of proof complexity. The structure must be preserved by the basic inference mechanism of the system in question if it is to remain useful, and QPROP's ability to speed the inner loop of unit propagation is a direct consequence of the structure present in the subsearch problem. Finally, learning itself can be thought of as a search for reasonably concise descriptions of large sections of the search space that contain no solutions - in other words, learning is the discovery of structure in the search space itself.
This is the setting against which the next two papers in this series are set. If so much of the progress in satisfiability techniques can be thought of as structure exploitation, then surely it is natural to attempt to understand and to exploit that structure directly. As we will see, not only do the techniques we have discussed work by exploiting structure, but they all exploit different instances of a single structure. The ZAP work is an attempt to understand, generalize and streamline previous results by setting them in this uniform setting.