SAT-Based Answer Set Programming

11 years 11 months ago
SAT-Based Answer Set Programming
The relation between answer set programming (ASP) and propositional satisfiability (SAT) is at the center of many research papers, partly because of the tremendous performance boost of SAT solvers during last years. Various translations from ASP to SAT are known but the resulting SAT formula either includes many new variables or may have an unpractical size. There are also well known results showing a one-to-one correspondence between the answer sets of a logic program and the models of its completion. Unfortunately, these results only work for specific classes of problems. In this paper we present a SAT-based decision procedure for answer set programming that (i) deals with any (non disjunctive) logic program, (ii) works on a SAT formula without additional variables, and (iii) is guaranteed to work in polynomial space. Further, our procedure can be extended to compute all the answer sets still working in polynomial space. The experimental results of a prototypical implementation show...
Enrico Giunchiglia, Yuliya Lierler, Marco Maratea
Added 30 Oct 2010
Updated 30 Oct 2010
Type Conference
Year 2004
Where AAAI
Authors Enrico Giunchiglia, Yuliya Lierler, Marco Maratea
Comments (0)