The time complexity of well-founded semantics for a general logic program P is known to be quadratic in the size of P, a result attributed to folklore in . A proof was given by Witteveen (1991). His analysis is based on Dowling and Gallier's result whereby satisfiability of Horn clauses can be tested in linear time . In Dowling and Gallier's approach it is actually a minimal model of a Horn theory that is computed in linear time. Since minimal models of Horn theories are equivalent to closures of rules without negation the result is directly applicable to well-founded semantics for general logic programs. It also applies to well-founded semantics for extended logic programs since for the computation of the least fixed point of respectively the complementary literals l and can be vi wed as two distinct atoms.
For the complexity analysis of our prioritized approach let n be the number of rules in a prioritized program . A straightforward implementation would model the application of in an outer loop and the computation of in an inner loop. Fortunately, we can combine the two loops into a single loop whose body is executed at most n times. The reason is that grows monotonically with X and grows monotonically with . Here is a nondeterministic algorithm for computing the least fixed point of :
Procedure WFS+In each step and denote the well-founded conclusions, respectively safe rules established so far. The body of the for-loop is executed at most n times and there are at most n rules that have to be checked for satisfaction of the if-condition. The if-condition itself can, according to the results of Dowling and Gallier, be checked in linear time: we need to establish which involves the computation of a minimal model of the monotonic counterparts of . We then have to eliminate the rules dominated by r form and compute another minimal model to see whether r is defeated.
Input: A prioritized logic program with |R| = n
Output: the least fixed point of
for i = 1 to n doif there is a rule such thatendfor
does not defeat r
More precisely, Dowling and Gallier show that the needed time is linear in the number of propositional constants. This number may be greater than n in principle. However, since literals that do not appear in the head of a rule must be false in the minimal model we can eliminate them accordingly and work with a set of rules that has at most n literals. This leads to an overall time complexity of .
It should be mentioned, however, that due to the use of rule schemata for transitivity and anti-symmetry of prioritized programs can be considerably larger than corresponding unprioritized programs. The transitivity schema, for instance, has instances. An implementation should, therefore, be based on an approach where instances are only generated when actually needed, or on other built in techniques that handle transitivity and anti-symmetry. Such techniques are beyond the scope of this paper.