Quantification and QPROP

We conclude our survey with an examination of ideas that have been used in trying to extend the Boolean work to cope with theories that are most naturally thought of using quantification of some sort. Indeed, as Boolean satisfiability engines are applied to ever larger problems, many of the theories in question are produced in large part by constructing the set of ground instances of quantified axioms such as

$$\forall{xyz}.[a(x,y) \wedge b(y,z) \rightarrow c(x,z)]$$ (42)

If $d$ is the size of the domain from which $x$, $y$ and $z$ are taken, this single axiom has $d^3$ ground instances. Researchers have dealt with this difficulty by buying machines with more memory or by finding clever axiomatizations for which ground theories remain manageably sized [Kautz SelmanKautz Selman1998]. In general, however, memory and cleverness are both scarce resources and a more natural solution needs to be found.

We will call a clause such as (42) quantified, and assume throughout this section that the quantification is universal as opposed to existential, and that the domains of quantification are finite.¹⁴

As we remarked at the beginning of this section, quantified clauses are common in encodings of realistic problems, and these problems have in general been solved by converting quantified clauses to standard propositional formulae. The quantifiers are expanded first (possible because the domains of quantification are finite), and the resulting set of predicates is then ``linearized'' by relabeling all of the atoms so that, for example, $a(2,3)$ might become $v_{24}$. The number of ground clauses produced is exponential in the number of variables in the quantified clause.