Abstract answer set solvers with backjumping and learning
Yuliya Lierler · Theory and Practice of Logic Programming · 2011
Abstract Nieuwenhuis et al. (2006. Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM 53(6), 937977 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, smodelscc, asp-sat with Learning (cmodels), and a newly designed and implemented algorithm sup. This approach to describe answer set solvers makes it easier to prove their correctness, to compare them, and to design new systems.