Show how to implement the stingy algorithm for Horn formula satisfiability in time that is linear in length of the formula (the no. of occurrences of literals in it.)

Use a directed graph, with one node per variable to represent the implications.)

(This is exercise 5.32 in the bookbyS. Dasgupta, C.H. Papadimitriou, and U.V. Vazirani)Below is an efficient algorithm I got from Logic for Computer Scientists/Propositional Logic/Horn clauses - Wikibooks, open books for an open world that is O(l).Algorithms

Deciding Satisfiability of Horn Formulae

- If there is a subformula of the kind label every occurrence of
AinF.- Apply the following rules until none of them is applicable:

- If is a subformula and are all labeled and
Bis not labeled then label every occurrence ofBinF.- If is a subformula and are all labeled then
Stop: UnsatisfiableStop: SatisfiableThe assignment iffAis labeled is a model.