Though the class of DNF formulas has very good computational properties, abduction remains a hard problem for it as a whole, even with additional restrictions. Recall that the TAUTOLOGY problem is the one of deciding whether a given DNF formula represents the identically true function, and that this problem is coNP-complete.
However, when is represented by a DNF projecting it onto
is
easy; indeed, the properties of projection show that it suffices to cancel
its literals that are not formed upon
. Consequently, if
is such a
DNF containing
terms, then a DNF
with
and containing at most
terms can be computed in time
.
Thus we can show that some subclasses of the class of all DNFs allow
polynomial abduction. We state the first result quite generally, but note
that its assumptions are satisfied by natural classes of DNFs: e.g., that of
Horn DNFs, i.e., those DNFs with at most one positive literal per
term; similarly, that of Horn-renamable DNFs, i.e., those that can be turned
into a Horn DNF by replacing some variables with their negation, and
simplifying double negations, everywhere in the formula; DNFs, those DNFs
with at most two literals per term. We omit the
proof of the following proposition, since it is essentially the same as that
of Proposition 2 (simply follow the execution of the
algorithm).
Finally, let us point out that with a very similar proof we can obtain
polynomiality for some problems obtained by strengthening the
restriction of Proposition 4 over , but weakening that
over
.