Answer Set Programming Based on Propositional Satisfiability |
| |
Authors: | Enrico Giunchiglia Yuliya Lierler Marco Maratea |
| |
Affiliation: | 1. STAR-Lab, DIST, University of Genova, viale Francesco Causa, 13-16145, Genova, Italy 2. Institut für Informatik, Erlangen-Nürnberg-Universit?t, Haberstr. 2, Erlangen, Germany 3. Department of Mathematics, University of Calabria, viale Pietro Bucci, Cubo 31b-87036, Rende, CS, Italy
|
| |
Abstract: | Answer set programming (ASP) emerged in the late 1990s as a new logic programming paradigm that 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. All these reductions, however, 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 ASPSAT, that (1) deals with any (nondisjunctive) logic program, (2) works on a propositional
formula without additional variables (except for those possibly introduced by the clause form transformation), and (3) is
guaranteed to work in polynomial space. From a theoretical perspective, we prove soundness and completeness of ASPSAT. From
a practical perspective, we have (1) implemented ASPSAT in Cmodels, (2) extended the basic procedures in order to incorporate the most popular SAT reasoning strategies, and (3) conducted an
extensive comparative analysis involving other state-of-the-art answer set solvers. The experimental analysis shows that our
solver is competitive with the other solvers we considered and that the reasoning strategies that work best on ‘small but
hard’ problems are ineffective on ‘big but easy’ problems and vice versa. |
| |
Keywords: | answer set programming propositional satisfiability |
本文献已被 SpringerLink 等数据库收录! |
|