Unique satisfiability of horn sets can be solved in nearly linear time
| Author(s) : | John S. Schlipf John Franco Kenneth A. Berman, |
| Publisher : | N/A |
| Publication Date : | 1995 |
| ISSN : | N/A |
| Abstract : | 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(ff(L) L) time, where L is the sum of the lengths of the clauses in I and ff 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. 1, |