Horn SAT algorithm using graphs

Question

For some restricted classes of logical formulae, the satisfiability problem can be solved efficiently in polynomial time or even linear. One such class is that of Horn formulae, which consist only of Horn clauses with at most one positive literal. I've heard that it is possible to solve Horn SAT in linear time using graphs, but couldn't find any implementation of such solution. Now I'm really interested whether it is possible and if it is, how would algorithm look like?

Answer 1

If you're familiar with Davis–Putnam–Logemann–Loveland, Horn clauses are a class of formulae that can be solved using one round of unit propagation, with no backtracking.

In graph terms, we do the obvious thing and set up a bipartite graph with variables on one side, clauses on the other, and edges to represent a variable appearing as a negative literal in a clause. We also have a work queue of clauses consisting of a single positive literal. While the work queue is not empty, pop any element, identify the node corresponding to the variable, and delete it and its neighbors. For each clause vertex that now has degree zero, one of two things happens. If that clause has a positive literal, then we add it to the work queue. Otherwise, we've proved that the formula is unsatisfiable. If we reach the end of the work queue without finding such a clause, then the formula is satisfiable, and one satisfying assignment is to set all variables that entered the work queue to true, and all others to false.