SciTech.blog
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).

Comments

Name: