Propositional Abduction with Implicit Hitting Sets
This work addresses efficiency issues in logic-based abduction for AI applications like explanation finding, but it is incremental as it builds on prior methods.
The paper tackles the problem of improving computational efficiency in propositional abduction by proposing algorithmic enhancements to an existing method based on implicit hitting sets and SAT solvers, resulting in exponential reductions in SAT solver calls and significant performance gains over state-of-the-art approaches.
Logic-based abduction finds important applications in artificial intelligence and related areas. One application example is in finding explanations for observed phenomena. Propositional abduction is a restriction of abduction to the propositional domain, and complexity-wise is in the second level of the polynomial hierarchy. Recent work has shown that exploiting implicit hitting sets and propositional satisfiability (SAT) solvers provides an efficient approach for propositional abduction. This paper investigates this earlier work and proposes a number of algorithmic improvements. These improvements are shown to yield exponential reductions in the number of SAT solver calls. More importantly, the experimental results show significant performance improvements compared to the the best approaches for propositional abduction.