Sciweavers

Share
NMR
2004
Springer

A SAT-based polynomial space algorithm for answer set programming

10 years 4 months ago
A SAT-based polynomial space algorithm for 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 sh...
Enrico Giunchiglia, Yuliya Lierler, Marco Maratea
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where NMR
Authors Enrico Giunchiglia, Yuliya Lierler, Marco Maratea
Comments (0)
books