Generating all abductive explanations for queries on propositional Horn theories
Technology (2003)
Available from www.springerlink.com
or
Abstract
Abduction is a fundamental mode of reasoning, which has taken on increasing importance in Artificial Intelligence (AI) and related disciplines. Computing abductive explanations is an important problem, and there is a growing literature on this subject. We contribute to this endeavor by presenting new results on computing multiple resp. all of the possibly exponentially many explanations of an abductive query from a propositional Horn theory represented by a Horn CNF. Here the issues are whether ...
Author-supplied keywords
Page 1
Generating all abductive explanations for queries on propositional Horn theories
Generating All Abductive Explanations
for Queries on Propositional Horn Theories
Thomas Eiter1 and Kazuhisa Makino2
1 Institut fu¨r Informationssysteme, Technische Universita¨t Wien,
Favoritenstraße 9-11, A-1040 Wien, Austria
eiter@kr.tuwien.ac.at
2 Division of Systems Science, Graduate School of Engineering Science, Osaka University,
Toyonaka, Osaka, 560-8531, Japan
makino@sys.es.osaka-u.ac.jp
Abstract. Abduction is a fundamental mode of reasoning, which has taken on
increasing importance in Artificial Intelligence (AI) and related disciplines. Com-
puting abductive explanations is an important problem, and there is a growing
literature on this subject. We contribute to this endeavor by presenting new results
on computing multiple resp. all of the possibly exponentially many explanations of
an abductive query from a propositional Horn theory represented by a Horn CNF.
Here the issues are whether a few explanations can be generated efficiently and, in
case of all explanations, whether the computation is possible in polynomial total
time (or output-polynomial time), i.e., in time polynomial in the combined size of
the input and the output. We explore these issues for queries in CNF and important
restrictions thereof. Among the results, we show that computing all explanations
for a negative query literal from a Horn CNF is not feasible in polynomial total
time unless P = NP, which settles an open issue. However, we show how to com-
pute under restriction to acyclic Horn theories polynomially many explanations in
input polynomial time and all explanations in polynomial total time, respectively.
Complementing and extending previous results, this draws a detailed picture of
the computational complexity of computing multiple explanations for queries on
Horn theories.
Keywords: Computational logic, abduction, propositional logic, Horn theories,
polynomial total time computation, NP-hardness.
1 Introduction
Abduction is a fundamental mode of reasoning, which was extensively studied by C.S.
Peirce [19]. It has taken on increasing importance in Artificial Intelligence (AI) and
related disciplines, where it has been recognized as an important principle of common-
sense reasoning (see e.g. [3]). Abduction has applications in many areas of AI and
Computer Science including diagnosis, database updates, planning, natural language
understanding, learning etc. (see e.g. references in [10]), where it is primarily used for
generating explanations.
This work was supported in part by the Austrian Science Fund (FWF) Project Z29-N04, by a
TU Wien collaboration grant, and by the Scientific Grant in Aid of the Ministry of Education,
Science, Sports, Culture and Technology of Japan.
M. Baaz and J.A. Makowsky (Eds.): CSL 2003, LNCS 2803, pp. 197–211, 2003.
c
© Springer-Verlag Berlin Heidelberg 2003
for Queries on Propositional Horn Theories
Thomas Eiter1 and Kazuhisa Makino2
1 Institut fu¨r Informationssysteme, Technische Universita¨t Wien,
Favoritenstraße 9-11, A-1040 Wien, Austria
eiter@kr.tuwien.ac.at
2 Division of Systems Science, Graduate School of Engineering Science, Osaka University,
Toyonaka, Osaka, 560-8531, Japan
makino@sys.es.osaka-u.ac.jp
Abstract. Abduction is a fundamental mode of reasoning, which has taken on
increasing importance in Artificial Intelligence (AI) and related disciplines. Com-
puting abductive explanations is an important problem, and there is a growing
literature on this subject. We contribute to this endeavor by presenting new results
on computing multiple resp. all of the possibly exponentially many explanations of
an abductive query from a propositional Horn theory represented by a Horn CNF.
Here the issues are whether a few explanations can be generated efficiently and, in
case of all explanations, whether the computation is possible in polynomial total
time (or output-polynomial time), i.e., in time polynomial in the combined size of
the input and the output. We explore these issues for queries in CNF and important
restrictions thereof. Among the results, we show that computing all explanations
for a negative query literal from a Horn CNF is not feasible in polynomial total
time unless P = NP, which settles an open issue. However, we show how to com-
pute under restriction to acyclic Horn theories polynomially many explanations in
input polynomial time and all explanations in polynomial total time, respectively.
Complementing and extending previous results, this draws a detailed picture of
the computational complexity of computing multiple explanations for queries on
Horn theories.
Keywords: Computational logic, abduction, propositional logic, Horn theories,
polynomial total time computation, NP-hardness.
1 Introduction
Abduction is a fundamental mode of reasoning, which was extensively studied by C.S.
Peirce [19]. It has taken on increasing importance in Artificial Intelligence (AI) and
related disciplines, where it has been recognized as an important principle of common-
sense reasoning (see e.g. [3]). Abduction has applications in many areas of AI and
Computer Science including diagnosis, database updates, planning, natural language
understanding, learning etc. (see e.g. references in [10]), where it is primarily used for
generating explanations.
This work was supported in part by the Austrian Science Fund (FWF) Project Z29-N04, by a
TU Wien collaboration grant, and by the Scientific Grant in Aid of the Ministry of Education,
Science, Sports, Culture and Technology of Japan.
M. Baaz and J.A. Makowsky (Eds.): CSL 2003, LNCS 2803, pp. 197–211, 2003.
c
© Springer-Verlag Berlin Heidelberg 2003
Page 2
198 Thomas Eiter and Kazuhisa Makino
In a logic-based setting, abduction can be viewed as the task to find, given a set
of formulas Σ (the background theory) and a formula χ (the query), a minimal set of
formulas E (an explanation) from a set of hypotheses H such that Σ plus E is satisfiable
and logically entails χ. Often considered is a scenario where Σ is a propositional Horn
theory, χ is a single literal or a conjunction of literals, and H contains literals (see [24,10]
and references therein). For use in practice, the computation of abductive explanations
in this setting is an important problem, for which well-known early systems such as
Theorist [20] or ATMS solvers [6,22] have been devised. Since then, there has been a
growing literature on this subject, indicating the need for efficient abductive procedures.
We refer to [18], which gives an excellent survey on intimately closely related problems
in computational logic. Note that much effort has been spent on studying various input
restrictions, cf. [14,4,13,25,8,7,10,23,24].
While computing some explanation of a query χ has been studied extensively in the
literature, the issue of computing multiple or even all explanations for χ has received
less attention. This problem is important since often one would like to select one out of
a set of alternative explanations according to a preference or plausibility relation; this
relation may be based on subjective intuition and thus difficult to formalize. As easily
seen, exponentially many explanations may exist for a query, and thus computing all
explanations inevitably requires exponential time in general, even in propositional logic.
However, it is of interest whether the computation is possible in polynomial total time
(or output-polynomial time), i.e., in time polynomial in the combined size of the input
and the output. Furthermore, if exponential space is prohibitive, it is of interest to know
whether a few explanations (e.g., polynomially many) can be generated in polynomial
time, as studied by Selman and Levesque [24].
Computing some explanation for a query χ which is a literal from a Horn theory is a
well-known polynomial problem. Selman and Levesque conjectured [24] that generating
O(n) many explanations for a positive literal is NP-hard, where n is the number of
propositional atoms in the language, even if it is guaranteed that there are only few
explanations overall. As shown in [11], this conjecture is not true unless P=NP. This
follows from the result of [11] that all explanations for an atom can be generated in
polynomial total time.
The status of generating all explanations for a negative literal χ = q from a Horn
CNF ϕ, however, remained open in [11]. Moreover, it was unclear whether a resolution-
style procedure similar to the one for query atoms in [11] could solve the problem in
polynomial total time. In this paper, we provide a negative answer to this question, by
showing that given a collection of explanations for a query χ = q from a Horn CNF ϕ,
deciding whether there is an additional explanation is NP-complete. Consequently, the
existence of a polynomial total time algorithm for computing all explanations implies
P=NP. However, for the well-known class of acyclic Horn theories (see e.g. [5,24,21,1])
we present an algorithm which enumerates all explanations for q with incremental poly-
nomial delay (i.e., in time polynomial in the size of the input and output so far), and thus
solves the problem in polynomial total time. Compared to explanations for an atomic
query q, intuitively cyclic dependencies between atoms make the problem difficult. For
completeness, a resolution-style procedure as in [11] needs to consider besides the input
In a logic-based setting, abduction can be viewed as the task to find, given a set
of formulas Σ (the background theory) and a formula χ (the query), a minimal set of
formulas E (an explanation) from a set of hypotheses H such that Σ plus E is satisfiable
and logically entails χ. Often considered is a scenario where Σ is a propositional Horn
theory, χ is a single literal or a conjunction of literals, and H contains literals (see [24,10]
and references therein). For use in practice, the computation of abductive explanations
in this setting is an important problem, for which well-known early systems such as
Theorist [20] or ATMS solvers [6,22] have been devised. Since then, there has been a
growing literature on this subject, indicating the need for efficient abductive procedures.
We refer to [18], which gives an excellent survey on intimately closely related problems
in computational logic. Note that much effort has been spent on studying various input
restrictions, cf. [14,4,13,25,8,7,10,23,24].
While computing some explanation of a query χ has been studied extensively in the
literature, the issue of computing multiple or even all explanations for χ has received
less attention. This problem is important since often one would like to select one out of
a set of alternative explanations according to a preference or plausibility relation; this
relation may be based on subjective intuition and thus difficult to formalize. As easily
seen, exponentially many explanations may exist for a query, and thus computing all
explanations inevitably requires exponential time in general, even in propositional logic.
However, it is of interest whether the computation is possible in polynomial total time
(or output-polynomial time), i.e., in time polynomial in the combined size of the input
and the output. Furthermore, if exponential space is prohibitive, it is of interest to know
whether a few explanations (e.g., polynomially many) can be generated in polynomial
time, as studied by Selman and Levesque [24].
Computing some explanation for a query χ which is a literal from a Horn theory is a
well-known polynomial problem. Selman and Levesque conjectured [24] that generating
O(n) many explanations for a positive literal is NP-hard, where n is the number of
propositional atoms in the language, even if it is guaranteed that there are only few
explanations overall. As shown in [11], this conjecture is not true unless P=NP. This
follows from the result of [11] that all explanations for an atom can be generated in
polynomial total time.
The status of generating all explanations for a negative literal χ = q from a Horn
CNF ϕ, however, remained open in [11]. Moreover, it was unclear whether a resolution-
style procedure similar to the one for query atoms in [11] could solve the problem in
polynomial total time. In this paper, we provide a negative answer to this question, by
showing that given a collection of explanations for a query χ = q from a Horn CNF ϕ,
deciding whether there is an additional explanation is NP-complete. Consequently, the
existence of a polynomial total time algorithm for computing all explanations implies
P=NP. However, for the well-known class of acyclic Horn theories (see e.g. [5,24,21,1])
we present an algorithm which enumerates all explanations for q with incremental poly-
nomial delay (i.e., in time polynomial in the size of the input and output so far), and thus
solves the problem in polynomial total time. Compared to explanations for an atomic
query q, intuitively cyclic dependencies between atoms make the problem difficult. For
completeness, a resolution-style procedure as in [11] needs to consider besides the input
Sign up today - FREE
Mendeley saves you time finding and organizing research. Learn more
- All your research in one place
- Add and import papers easily
- Access it anywhere, anytime
Start using Mendeley in seconds!
Readership Statistics
4 Readers on Mendeley
by Discipline
25% Mathematics
by Academic Status
25% Other Professional
25% Researcher (at an Academic Institution)
25% Professor
by Country
50% Germany
25% Japan
25% United States


