A lower bound for answer set solver computation

We build upon recent work by Lierler that defines 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 define 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 definitions and rules that can be seen as connecting the cycles. © AEPIA and the authors.