In this paper, we consider the Unique-SAT problem for Horn formulas (Unique-HornSAT). We use directed hypergraphs to represent Horn formulas, and devise a solution method based on a hypergraph transformation technique. In the implementation, we solve a particular disjoint set union problem for which linear amortized time algorithms are known. As a result, we obtain a linear time algorithm for Unique-HornSAT.
A linear time algorithm for unique Horn satisfiability / Pretolani, Daniele. - In: INFORMATION PROCESSING LETTERS. - ISSN 0020-0190. - STAMPA. - 48 (2):(1993), pp. 61-66. [10.1016/0020-0190(93)90178-C]