On the relation among answer set solvers
Annals of Mathematics and Artificial Intelligence, 53 (1):
169--204 (Aug 1, 2008)DOI: 10.1007/s10472-009-9113-1
Abstract
Abstract In this paper, we study the relation among Answer Set Programming (ASP) systems from a computational point of view. We consider smodels, dlv, and cmodels ASP systems based on stable model semantics, the first two being native ASP systems and the last being a SAT-based system. We first show that smodels, dlv, and cmodels explore search trees with the same branching nodes (assuming, of course, a same branching heuristic) on the class of tight logic programs. Leveraging on the fact that SAT-based systems rely on the deeply studied Davis–Logemann–Loveland (dll) algorithm, we derive new complexity results for the ASP procedures. We also show that on nontight programs the SAT-based systems are computationally different from native procedures, and the latter have computational advantages. Moreover, we show that native procedures can guarantee the ” correctness” of a reported solution when reaching the leaves of the search trees (i.e., no stability check is needed), while this is not the case for SAT-based procedures on nontight programs. A similar advantage holds for dlv in comparison with smodels if the ” well-founded” operator is disabled and only Fitting's operator is used for negative inferences. We finally study the ” cost” of achieving such advantages and comment on to what extent the results presented extend to other systems.