Solving HornSAT in linear time

Recently, i wanted to program a simple horn sat solver for a project (turned out i didn't need it, oh well).
I couldn't find anything on the net (in reasonable time) about how to solve HornSAT in linear time, only references to that it's possible. The naive approach, however, at least the one i took, has quadratic worst-case complexity. Now i thought i might spread the knowledge a bit about how to solve the horn satisfiability problem in linear time.
See also Unit Propagation

---

1.) build a directed (bipartite) graph, connecting the Horn clauses to their respective positive literal (if they have one), and connecting the literals to all clauses where they appear negated.
2.)[UPDATE] for every clause c not containing a negated literal, do {
if c has no positive literal STOP -> unsatisfiable
else propagate(c)
}

3.) finally, the function for the unit propagation:

propagate(c) :-
if the positive literal of c (p) is not yet marked true {

mark p true
for all (p,c') in the Edge set of the graph{
remove p from c'
if c' has no more negated literals, propagate(c')
}

}

---

The marked literals form the minimal model of that Horn formula.

Because every literal is only marked true once, the whole algorithm runs in linear time (with respect to the number of literals, because of the graph building).

[Update]
While thinking about this some more, i figured the above algorithm is only better than the naive one, if the number of literals is in O(#clauses²). For completeness, here the algorithm i call the "naive":

---

while there exists a clause c without negative literals{

if c has no positive literal then STOP -> formula not satisfiable;
mark the variable of the positive literal of c as true;
for all clauses c'  remove the just marked literal from the list of negated literals of c'

}

---

Let c be the number of clauses and l the number of literals.
With the proper implementation, the naive algorithm can run in O(min(c², cl)). This is better then the algorithm above if l is in Ω(c²).
We can easily check this by summing the sizes of the sets of negated literals, which can be done in O(c). If we wire this all together, we get an algorithm in O(min(l,c²)), as c is in O(l).

Here is also a paper on linear time algorithms for Horn Sat: Link