Abstract Answer Set Solvers with Learning

TL;DR

This paper introduces a unified transition system framework for answer set solvers, facilitating correctness proofs, comparisons, and new system designs for logic programming algorithms.

Contribution

It extends the transition system approach to multiple answer set solvers, including a new algorithm, enabling systematic analysis and development.

Findings

Framework simplifies correctness proofs.

Enables comparison of different solvers.

Supports design of new answer set algorithms.

Abstract

Nieuwenhuis, Oliveras, and Tinelli (2006) showed how to describe enhancements of the Davis-Putnam-Logemann-Loveland algorithm using transition systems, instead of pseudocode. We design a similar framework for several algorithms that generate answer sets for logic programs: Smodels, Smodels-cc, Asp-Sat with Learning (Cmodels), and a newly designed and implemented algorithm Sup. This approach to describing answer set solvers makes it easier to prove their correctness, to compare them, and to design new systems.