Finding satisfying assignments for the variables involved in aset of constraints can be cast as a (bounded) model generationproblem: search for (bounded) models of a theory in somelogic. The state-of-the-art approach for bounded model generationfor rich knowl- edge representation languages like Answer SetProgramming (ASP) and FO(·) and a CSP modeling language such asZinc, is ground-and-solve: reduce the theory to a ground orpropositional one and apply a search algorithm to the resultingtheory. An important bottleneck is the blow-up of the size ofthe theory caused by the grounding phase. Lazily grounding thetheory during search is a way to overcome this bottleneck. Wepresent a theoretical framework and an implementation in thecontext of the FO(·) knowledge representation language. Insteadof grounding all parts of a theory, justifications are derivedfor some parts of it. Given a partial assignment for the groundedpart of the theory and valid justifications for the formulas ofthe non-grounded part, the justifications provide a recipe toconstruct a complete assignment that satisfies the non-groundedpart. When a justification for a particular formula becomesinvalid during search, a new one is derived; if that fails, theformula is split in a part to be grounded and a part that can bejustified. Experimental results illustrate the power andgenerality of this approach.
展开▼
