A linear time algorithm for unique Horn satisfiability