Paper Info
Title
Implicit Hitting Set Algorithms for Reasoning Beyond NP.
Abstract
Lifting a recent proposal by Moreno-Centeno and Karp, 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.
Year
Venue
Field
2016
KR
Maximum satisfiability problem,Polynomial hierarchy,Computer science,Satisfiability,Boolean satisfiability problem,Algorithm,Theoretical computer science,Integer programming,Solver,Semantics,Encoding (memory)
DocType
Citations 
PageRank 
Conference
4
0.40
References 
Authors
42
3
Name
Order
Citations
PageRank
Paul Saikko1333.98
Johannes Peter Wallner220120.62
Matti Järvisalo358151.00