Partial grounding

Model expansion is the task underlying many paradigms for declarative solving of computationally hard search problems such as scheduling, planning, and formal verification. We develop a technique to solve model expansion tasks involving arithmetic and other infinite secondary structures. Unlike previously developed methods, our technique produces quantifier-free formulas suitable for tools that are specially designed for arithmetic such as satisfiability modulo theories (SMT) solvers. The novelty is in that our method leaves part of the specification not grounded. We design new algorithms which first perform partial grounding, and then take a quantifier-free formula and produce a formula suitable for solving using SMT. An SMT solver is called on the resulting formula. We describe how we constructed a software tool for partial grounding and list several example inputs and the results of using the Yices SMT solver on the outputs.