  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
\Sigma_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.
