Backdoors to Abduction
This work addresses a fundamental bottleneck in AI reasoning for applications such as fault diagnosis and planning, though it is incremental as it builds on existing structural methods.
The authors tackled the high computational complexity of propositional Abduction, which is Σ_2^P-complete and lacks polynomial transformations to SAT, by using structural properties like small backdoor sets to develop fixed-parameter tractable transformations to SAT, enabling the use of modern SAT solvers for Abduction.
Abductive reasoning (or Abduction, for short) is among the most fundamental AI reasoning methods, with a broad range of applications, including fault diagnosis, belief revision, and automated planning. Unfortunately, Abduction is of high computational complexity; even propositional Abduction is Σ_2^P-complete and thus harder than NP and coNP. This complexity barrier rules out the existence of a polynomial transformation to propositional satisfiability (SAT). In this work we use structural properties of the Abduction instance to break this complexity barrier. We utilize the problem structure in terms of small backdoor sets. We present fixed-parameter tractable transformations from Abduction to SAT, which make the power of today's SAT solvers available to Abduction.