Sciweavers

JAR
2006

Answer Set Programming Based on Propositional Satisfiability

13 years 3 months ago
Answer Set Programming Based on Propositional Satisfiability
Answer Set Programming (ASP) emerged in the late 1990s as a new logic programming paradigm which has been successfully applied in various application domains. Also motivated by the availability of efficient solvers for propositional satisfiability (SAT), various reductions from logic programs to SAT were introduced in the past. All these reductions either are limited to a subclass of logic programs, or introduce new variables, or may produce exponentially bigger propositional formulas. In this paper, we present a SAT-based procedure, called ASP-SAT, that (i) deals with any (non disjunctive) logic program, (ii) works on a propositional formula without additional variables (except for those possibly introduced by the clause form transformation), and (iii) is guaranteed to work in polynomial space. From a theoretical perspective, we prove soundness and completeness of ASP-SAT. From a practical perspective, we have (i) implemented ASP-SAT in Cmodels, (ii) extended the basic procedures in o...
Enrico Giunchiglia, Yuliya Lierler, Marco Maratea
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2006
Where JAR
Authors Enrico Giunchiglia, Yuliya Lierler, Marco Maratea
Comments (0)