SciTech.blog

Abduction as satisfiability

24 Feb 2018, 14:36 • logic

Effectively propositional abductive problems can be cast in terms of satisfiability. This post shows when it's possible and how to do it.

First-order abductive rules consist of an antecedent (on the left) and a consequent (on the right), whereby inference happens by backchaining on a rule, that is, the consequent is given (observed or assumed) and the antecedent can be assumed in order to explain some observables. In symbols

$A \supset C$

Let $$V(\varphi)$$ be the set of all variables occurring in a formula $$\varphi$$. A theory is effectively propositional if the observables are all ground and $$V(A)\subseteq V(C)$$ for all rules. An effectively propositional theory can be straightforwardly converted into a propositional theory so our rules now look like

$p_1 \land \dots \land p_n \supset q_1 \land \dots \land q_m$

where $$p_i,q_i$$ are propositional variables. However these rules are abductive and SAT solvers only work with classical deductive rules. We'll first introduce new propositional variables $$r_i$$ for the ground rules of the theory. We'll now add a few necessary conditions to the theory:

$\begin{array}{c} r_i \rightarrow c \\ r_i \rightarrow a \\ \end{array}$

for all propositional variables $$c$$ in the consequent of $$r_i$$ and $$a$$ in the antecedent of $$r_i$$. We'll also need

$\neg r_i \lor \neg r_j$

for all $$r_i,r_j$$ that share a common variable in their consequents, since a literal can be explained by at most one rule. We'll also need $$o_i$$ for all observables and $$r_i\rightarrow e_a$$ for all variables in the antecedent of $$r_i$$. For every variable representing a literal we'll then add $$o_i \lor e_i$$, that is, every literal in the proof is either observed or assumed by backchaining on a rule. These additional rules ensure that all proofs are correct in the sense that $$I \vdash O$$ and there are no extraneous literals.

We now have a set of classical propositional clauses so we can use a SAT solver to generate abductive proofs (it's easy to see that there's a one-to-one correspondence between abductive proofs and propositional valuations).