On the Foundations of Answer Set Programming
Victor W. Marek, Jeffrey B. Remmel · 2001
Schlipf (Schlipf 1995) proved that the Stable Logic Programming solves all NP decision problems. We extend Schlipf’s result to all search problems in the class NP. Moreover, we do this in a uniform way as defined in (Marek & Truszczyfiski 1999). Specifically, we show that there is a single DATALOG ~ program Pr~ so that for every Turing machine T, every polynomial with nonnegative coedicients p, every positive integer n and an input cr of size at most n over a fixed alphabet E there is a polynomial-time encoding of the machine M and the input as an extensional database edbM,p,, so that there is a one-to-one correspondence between the stable models of edbM,p,, U P~ and accepting computations of the machine M that reach the final state in at most p(n) steps. The decoding of computations form stable models is done in polynomial (in fact linear), time as well.