Unit Propagation

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 $a(2,3)$ might well take several times longer than finding the value assigned to the equivalent $v_{24}$. 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.