Blending lazy-grounding and CDNL search for answer-set solving. (English) Zbl 1491.68262

Balduccini, Marcello (ed.) et al., Logic programming and nonmonotonic reasoning. 14th international conference, LPNMR 2017, Espoo, Finland, July 3–6, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10377, 191-204 (2017).
Summary: Efficient state-of-the-art answer-set solvers are two-phased: first grounding the input program, then applying search based on conflict-driven nogood learning (CDNL). The latter provides superior search performance but the former causes exponential memory requirements for many ASP programs. Lazy-grounding avoids this grounding bottleneck but exhibits poor search performance. The approach here aims for the best of both worlds: grounding and solving are interleaved, but there is a solving component distinct from the grounding component. The solving component works on (ground) nogoods, employs conflict-driven first-UIP learning and enables heuristics. Guessing is on atoms that represent applicable rules, atoms may be one of true, false, or must-be-true, and nogoods have a distinguished head literal. The lazy-grounding component is loosely coupled to the solver and may yield more ground instances than necessary, which avoids re-grounding whenever the solver moves from one search branch to another. The approach is implemented in the new ASP solver Alpha.
For the entire collection see [Zbl 1367.68005].


68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
68N17 Logic programming
Full Text: DOI