How to adapt DPLL to solve HORNSAT?
Horn formulas are always satisfiable unless there is at least one unit clause that contains a positive literal.  (Otherwise assigning false to all the variables guarantees the formula would be satisfied.)  The procedure in that case is to unit propagate all unit clauses that contain a positive literal and unit propagate any such new clauses as they occur.  Once this task is completed, if the remaining formula contains no empty clauses then the Horn formula is satisfiable.