@inproceedings{SaikkoWJ:KR2016, author = {Paul Saikko and Johannes Peter Wallner and Matti J\"arvisalo}, title = {Implicit Hitting Set Algorithms for Reasoning Beyond {NP}}, booktitle = {Proceedings of the 15th International Conference on Principles of Knowledge Representation and Reasoning (KR 2016)}, editor = {Chitta Baral and James P. Delgrande and Frank Wolter}, pages = {104--113}, publisher = {AAAI Press}, year = {2016}, } Abstract: Lifting a recent proposal, we propose a general framework for so-called implicit hitting set algorithms for reasoning beyond NP. The framework is motivated by empirically successful specific instantiations of the approach---based on interactions between a Boolean satisfiability (SAT) solver and an integer programming (IP) solver---in the context of maximum satisfiability (MaxSAT). The framework opens up opportunities for developing implicit hitting set algorithms for various important reasoning problems in KR by implementing domain-specific reasoning modules with SAT and IP solvers. We detail instantiations of the framework for the minimum satisfiability problem---as a natural dual of MaxSAT---and, as a central KR problem, for propositional abduction, covering the second level of the polynomial hierarchy. We show empirically that an implementation of the instantiation for propositional abduction surpasses the efficiency of an approach based on encoding and solving propositional abduction instances as disjunctive logic programming under answer set semantics. We also study key properties of the general framework.