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

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.^{14}

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, might become . The number of ground clauses produced is exponential in the number of variables in the quantified clause.