Lifted unit propagation

Recent emergence of effective solvers for propositional satisfiability (SAT) and related problems has led to new methods for solving computationally challenging industrial problems, such as NP-hard search problems in planning, software design, and hardware verification. This has produced a demand for tools which allow users to write high level problem specifications which are automatically reduced to SAT. We consider the case of specifications in first order logic with reduction to SAT by grounding. For realistic problems, the resulting SAT instances can be prohibitively large. A key technique in SAT solvers is unit propagation, which often significantly reduces instance size before search for a solution begins. We define ”lifted unit propagation”, which is executed before grounding. We show that instances produced by a grounding algorithm with lifted unit propagation are never larger than those produced by normal grounding followed by UP, and demonstrate experimentally that they are sometimes much smaller.