Unique satisfiability of Horn sets can be solved in nearly linear time Original Research Article

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(α(L)∗L) time, where L is the sum of the lengths of the clauses in I and α is the inverse Ackermann function. It is also shown that if L⩾A∗log (A) where A is the number of distinct proposition letters then unique satisfiability can be determined in O(L) time.