Finding optimal solutions to the abduction problem in separation logic

Max Kanovich

Abduction, the problem of discovering hypotheses that support a conclusion, has mainly been studied in the context of philosophical logic and AI. Recently, the abduction principle -- given A and B, find a non-trivial X such that A*X entails B, is one of the powerful practical tools for iterated deduction and hypothesis formation to 'dig information out of bare code'. The important part of the problem is to find optimal/minimal solutions X.

We study the complexity of finding optimal/minimal solutions to the abduction problem for a relevant fragment of separation logic over 'symbolic heaps' which include a basic 'points-to' predicate, and an inductive predicate for describing linked-list segments.

We show that the complexity of finding minimal solutions ranges from $NP$-complete to polytime for different sub-problems. The following parametrized complexity is of great practical and theoretical importance -- that is, the NP-completeness notwithstanding, there is a polytime procedure for finding minimal solutions to abduction but degree of the polynomial is proportional to the number of 'list segment' subformulas in B.

This is joint work with Nikos Gorogiannis and Peter O'Hearn.