A Comparison of Different Techniques for Grounding Near-Propositional CNF Formulae
Stephan Schulz · 2002
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. How-ever, naive approaches to grounding can generate extremely large ground formulae. We investigate various means to re-duce the number of ground instances generated and show that we can increase the number of problems that can be handled with reasonable resources.