UNIQUE SATISFIABILITY OF HORN SETS CAN BE SOLVED IN NEARLY LINEAR-TIME

If a Horn set I has a single satisfying truth assignment or model then that model is said to be unique for I. The question of determining whether a unique model exists for a given Horn set I is shown to be solved in O(alpha(L)*L) time, where L is the sum of the lengths of the clauses in I and alpha is the inverse Ackermann function. It is also shown that if L greater than or equal to A*log(A) where A is the number of distinct proposition letters then unique satisfiability can be determined in O(L) time.