INTELIGENCIA ARTIFICIAL, Vol 14, No 48 (2010)

A Lower Bound for Answer Set Solver Computation

Stefania Costantini, Alessandro Provetti

Abstract


We build upon recent work by Lierler that de nes an abstract framework for describing the algorithm
underlying many of the existing answer set solvers (for answer set programs, based upon the Answer Set Semantics), considering in particular Smodels and SUP. We de ne a particular class of programs, called AOH, and prove that the computation that the abstract solver performs actually represents a lower bound for deciding inconsistency of logic programs under the Answer Set Semantics. The main result is that for a given AOH program with n atoms, an algorithm that conforms to Lierler's abstract model needs (n) steps before exiting with failure (no answer set exists). We argue that our result holds for every logic program that, like AOH programs, contains cyclic de nitions and rules that can be seen as connecting the cycles.

Full Text: PDF