Computationally Hard Problems for Logic Programs under Answer Set Semantics

Showing that a problem is hard for a model of computation is one of the most challenging tasks in theoretical computer science, logic and mathematics. For example, it remains beyond reach to find an explicit problem that cannot be computed by polynomial size propositional formulas (PF). As a model of computation, logic programs (LP) under answer set semantics are as expressive as PF and also NP-complete for satisfiability checking. In this article, we show that the PAR problem is hard for LP, i.e., deciding whether a binary string contains an odd number of 1's requires exponential size LP. The proof idea is first to transform logic programs into equivalent boolean circuits and then apply a probabilistic method known as random restriction to obtain an exponential lower bound. Based on the main result, we generalize a sufficient condition for identifying hard problems for LP and give a separation map for an LP family from a computational point of view, whose members are all equally expressive and share the same reasoning complexity.