CNF can be easily converted into a formula that uses only
NOT operations, using the fact that
a OR b = NOT(NOT(a) AND NOT(b)), in linear time.
This formula can be represented as a graph, where an edge goes down to
F depending on whether that variable or intermediate node is
ANDed without or with
This problem can be further reduced to Horn satisfiability as the picture above shows, by using the fact that
(x=>y) = NOT(x) OR y and introducing substitution variables so to satisfy the requirement for all clauses to be Horn clauses. In turn, Horn satisfiability can be solved in linear time.
So it seems that boolean satisfiability can be solved in linear time with this approach.