# Lazy Model Expansion: Interleaving Grounding with Search

arXiv: https://arxiv.org/abs/1402.6889 · HTML: https://mlsanity.com/paper/1402.6889/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 27 Feb 2014.

## Built on by (most cited first, 3 of 3)

- [Answer Set Planning: A Survey](https://mlsanity.com/paper/2202.05793/) (2022)
- [Specifying and Exploiting Non-Monotonic Domain-Specific Declarative Heuristics in Answer Set Programming](https://mlsanity.com/paper/2209.09066/) (2022)
- [FOLASP: FO(.) as Input Language for Answer Ser Solvers](https://mlsanity.com/paper/2108.04020/) (2021)

## Abstract (arXiv)

Finding satisfying assignments for the variables involved in a set of constraints can be cast as a (bounded) model generation problem: search for (bounded) models of a theory in some logic. The state-of-the-art approach for bounded model generation for rich knowledge representation languages, like ASP, FO(.) and Zinc, is ground-and-solve: reduce the theory to a ground or propositional one and apply a search algorithm to the resulting theory. An important bottleneck is the blowup of the size of the theory caused by the reduction phase. Lazily grounding the theory during search is a way to overcome this bottleneck. We present a theoretical framework and an implementation in the context of the FO(.) knowledge representation language. Instead of grounding all parts of a theory, justifications are derived for some parts of it. Given a partial assignment for the grounded part of the theory and valid justifications for the formulas of the non-grounded part, the justifications provide a recipe to construct a complete assignment that satisfies the non-grounded part. When a justification for a particular formula becomes invalid during search, a new one is derived; if that fails, the formula is split in a part to be grounded and a part that can be justified. The theoretical framework captures existing approaches for tackling the grounding bottleneck such as lazy clause generation and grounding-on-the-fly, and presents a generalization of the 2-watched literal scheme. We present an algorithm for lazy model expansion and integrate it in a model generator for FO(ID), a language extending first-order logic with inductive definitions. The algorithm is implemented as part of the state-of-the-art FO(ID) Knowledge-Base System IDP. Experimental results illustrate the power and generality of the approach.