Backdoors to Tractable Answer-Set Programming
Johannes Klaus Fichte and Stefan Szeider
We present a novel and unifying approach to the efficient evaluation of propositional answer-set programs. Our approach is based on the notion of backdoors which are small sets of atoms that represent "clever reasoning shortcuts" through the search space. Backdoors are widely used in the area of Propositional Satisfiability and Constraint Satisfaction. We show how this notion can be adapted to the nonmonotonic setting and how it allows to represent and augment various known tractable subproblems, such as the evaluation of Horn and acyclic programs. In order to use backdoors we need to find them first. We utilize recent advances in fixed-parameter algorithmics to detect small backdoors. We show that the evaluation of propositional answer-set programs is fixed-parameter tractable when parameterized by the size of backdoors. Hence backdoor size provides a structural parameter similar to the treewidth parameter considered by Jakl, Pichler, and Woltran (IJCAI'09). We show that backdoor size and treewidth are orthogonal, hence there are instances that are hard for one and easy for the other parameter. We complement our theoretical results with a first empirical evaluation. Keywords: Backdoor sets, fixed-parameter tractability, parameterized complexity, answer-set programming, nonmonotonic reasoning