Abstract Answer Set Solvers with Learning
Artificial Intelligence
2010-01-07 v1 Logic in Computer Science
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.
Cite
@article{arxiv.1001.0820,
title = {Abstract Answer Set Solvers with Learning},
author = {Yuliya Lierler},
journal= {arXiv preprint arXiv:1001.0820},
year = {2010}
}
Comments
Long version of the paper that will appear in special issue of Theory and Practice of Logic Programming