Abstract answer set solvers

Nieuwenhuis, Oliveras, and Tinelli showed how to describe enhancements of the Davis-Putnam-Logemann-Loveland algorithm using transition systems, in-stead of pseudocode. We design a similar framework for three algorithms that generate answer sets for logic programs: SMODELS, ASP-SAT with Backtracking, and a newly designed and implemented algorithm SUP. This approach to describ-ing answer set solvers makes it easier to prove their correctness, to compare them, and to design new systems.