Stephan Schulz: A Comparison of Different Techniques for Grounding
                Near-Propositional CNF Formulae

Abstract:

A near-propositional CNF formula is a first-order formula (in clause
normal form) with a finite Herbrand universe. For this class of
problems, the validity problem can be decided by a combination of
grounding and propositional reasoning. However, naive approaches to
grounding can generate extremely large ground formulae. We investigate
various means to reduce the number of ground instances generated and
show that we can increase the number of problems that can be handled
with reasonable resources.