24
On Computing All Abductive Explanations from a
Propositional Horn Theory
THOMAS EITER
Vienna University of Technology
AND
KAZUHISA MAKINO
University of Tokyo
Abstract. Abduction is a fundamental mode of reasoning with applications in many areas of AI
and Computer Science. The computation of abductive explanations is an important computational
problem, which is at the core of early systems such as the ATMS and Clause Management Systems
and is intimately related to prime implicate generation in propositional logic. Many algorithms have
been devised for computing some abductive explanation, and the complexity of the problem has
been well studied. However, little attention has been paid to the problem of computing multiple
explanations, and in particular all explanations for an abductive query. We fill this gap and consider
the computation of all explanations of an abductive query from a propositional Horn theory, or of
a polynomial subset of them. Our study pays particular attention to the form of the query, ranging
from a literal to a compound formula, to whether explanations are based on a set of abducible
literals and to the representation of the Horn theory, either by a Horn conjunctive normal form
(CNF) or model-based in terms of its characteristic models. For these combinations, we present either
tractability results in terms of polynomial total-time algorithms, intractability results in terms of
Dedicated to the memory of Marco Cadoli.
Most of the results in this article appeared in preliminary form in Proceedings of the 18th National
Conference on Article Intelligence (AAAI ’02), (Edmonton, Alb., Canada, July 28–Aug. 1), AAAI
Press, 2002; Proceedings of the 12th Annual Conference of the EASCL (CSL 2003), (Viena, Austia,
Aug. 25–30), Lecture Notes in Computer Science, Springer-Verlag, New York, 2003; and Proceedings
of the 6th International Conference on Discovery Science (DS 2003) (Sapporo, Japan, Oct. 17–19),
Lecture Notes in Computer Science, Springer-Verlag, New York, 2003.
This work was supported in part by the Austrian Science Fund (FWF) Project Z29-N04; by a TU
Wien collaboration grant; by the Wolfgang Pauli Institute, Vienna; and by the Scientific Grant in Aid
of the Ministry of Education, Science, Sports, Culture and Technology of Japan.
Authors’ addresses: T. Eiter, Institut fu¨r Informationssysteme, Technische Universita¨t Wien,
Favoritenstrasse 9-11, 1040 Wien, Austria, e-mail: eiter@kr.tuwien.ac.at; K. Makino, Department
of Mathematical Informatics, Graduate School of Information and Technology, University of Tokyo,
Tokyo, 113-8656, Japan, e-mail: makino@mist.i.u-tokyo.ac.jp.
Permission to make digital or hard copies of part or all of this work for personal or classroom use is
granted without fee provided that copies are not made or distributed for profit or direct commercial
advantage and that copies show this notice on the first page or initial screen of a display along with the
full citation. Copyrights for components of this work owned by others than ACM must be honored.
Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, to redistribute
to lists, or to use any component of this work in other works requires prior specific permission and/or
a fee. Permissions may be requested from Publications Dept., ACM, Inc., 2 Penn Plaza, Suite 701,
New York, NY 10121-0701 USA, fax +1 (212) 869-0481, or permissions@acm.org.
C©
2007 ACM 0004-5411/2007/10-ART24 $5.00 DOI 10.1145/1284320.1284323 http://doi.acm.org/
10.1145/1284320.1284323
Journal of the ACM, Vol. 54, No. 5, Article 24, Publication date: October 2007.

24:2 T. EITER AND K. MAKINO
nonexistence of such algorithms (unless P = NP), or semi-tractability results in terms of solvability
in quasi-polynomial time, established by polynomial-time equivalence to the problem of dualizing
a monotone CNF expression. Our results complement previous results in the literature, and refute a
longstanding conjecture by Selman and Levesque. They elucidate the complexity of generating all
abductive explanations and shed light on related problems such as generating sets of restricted prime
implicates of a Horn theory. The algorithms for tractable cases can be readily applied for generating
a polynomial subset of explanations in polynomial time.
Categories and Subject Descriptors: F.2.2 [Analysis of Algorithms and Problem Complexity]:
Nonnumerical Algorithms and Problems—Complexity of proof procedures, computations on discrete
structures; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic—Computa-
tional logic, mechanical theorem proving; I.2.3 [Artificial Intelligence]: Deduction and Theorem
Proving—Answer/reason extraction, resolution; I.2.4 [Artificial Intelligence]: Knowledge Repre-
sentation Formalisms and Methods
General Terms: Algorithms, Theory
Additional Key Words and Phrases: Abduction, propositional logic, Horn theories, polynomial total-
time computation, enumeration algorithms, dualization problem, model-based reasoning, character-
istic set, prime implicates, tractability, NP-hardness
ACM Reference Format:
Eiter, T. and Makino, K. 2007. On Computing all abductive explanations from a propositional Horn
theory. J. ACM 54, 5, Article 24 (October 2007), 54 pages. DOI = 10.1145/1284320.1284323
http://doi.acm.org/10.1145/1284320.1284323
1. Introduction
Abduction is a fundamental mode of reasoning and has been recognized as an
important principle of common-sense reasoning (see, e.g., Brewka et al. [1997]).
It has applications in many areas of AI and Computer Science including diagnosis,
planning, learning, natural language understanding, database updates and many
others (see, e.g., the discussions and references in Console et al. [1995], Eiter and
Gottlob [1995], Eiter et al. [1997], and Kakas et al. [1998]).
In a logic-based setting, abduction can be defined as the task, given a set of
formulas  (the background theory) and a formula χ (the query), of finding a set
of formulas E (an explanation) from a set of hypotheses (the abducibles) such that
 plus E is satisfiable and logically entails χ . Applying Occam’s razor, the set E
should satisfy the principle of parsimony and be as simple as possible. While there
is no unique way of capturing this, it is widely agreed that explanations should be
nonredundant, that is, no constituents may be dropped without loss of the expla-
nation property. This property, usually referred to as minimality of explanations,
is also satisfied by other formalizations of explanations, for example, those based
on the cardinality of E or on a probability distribution over the abducibles. In this
article, we deal with the generic class of nonredundant explanations and refer to
them simply as explanations.
The computation of abductive explanations is a problem with important practical
consequences. Well-known early systems such as Theorist [Poole 1989] and ATMS
solvers [de Kleer 1986; Reiter and de Kleer 1982] have been devised to address it.
Since then, there has been a vastly growing literature on the subject, indicating the
need for efficient abductive procedures. We refer to Marquis [2000], which gives
an excellent survey on closely related problems in logic. As computing abductive
explanations is generally intractable, much effort has been spent on identifying
tractable fragments, cf. Friedrich et al. [1990], Bylander [1991], Eshghi [1993],
Journal of the ACM, Vol. 54, No. 5, Article 24, Publication date: October 2007.