As a final remark, an interesting observation is that the effect of the transformation presented in (Anger et al. 2006), which enables smodels to branch on the bodies of rules, having an exponential effect on the proof complexity of a particular program family, can be equivalently obtained by applying the ASP extension rule. This may in part explain the effect of adding redundancy on the number of decision made by smodels.

## 7 Conclusions

We introduce Extended ASP Tableaux, an extended tableau calculus for normal logic programs under the stable model semantics. We study the strength of the calculus, showing a tight correspondence with Extended Resolution, which is among the most powerful known propositional proof systems. This sheds further light on the relation of ASP and propositional satisfiability solving and their underlying proof systems, which we believe to be for the benefit of both of the communities.

Our experiments show the intricate nature of the interplay between redundant problem structure and the hardness of solving ASP instances. We conjecture that more systematic use of the extension rule is possible and may even yield performance gains by considering in more detail the structural properties of programs in particular problem domains. One could also consider implementing branching on any possible formula inside a solver. However, this would require novel heuristics, since choosing the formula to branch on from the exponentially many alternatives is nontrivial and is not applied in current solvers. We find this an interesting future direction of research. Another important research direction set forth by this study is a more in depth investigation into the effect of program simplification on the hardness of solving ASP instances.

## 8 Acknowledgements

The authors thank Ilkka Niemelä for comments on a manuscript of this article.

Financial support from Helsinki Graduate School in Computer Science and Engineering, Academy of Finland (grants \#211025 and \#122399), Emil Aaltonen Foundation, Nokia Foundation, Finnish Foundation for Technology Promotion TES, Jenny and Antti Wihuri Foundation (MJ), and Finnish Cultural Foundation (EO)
is gratefully acknowledged

## References 24
