A Lower-bound for Answer Set solver Computation

We build upon recent work by Lierler that denes 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 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. For that class of programs, given a program composed of n atoms a solver adopting this algorithm must perform no less than n steps. We then argue that this result can be extrapolated to every logic program.