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]
A linear time algorithm for unique Horn satisfiability
PRETOLANI, Daniele
1993
Abstract
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.
Pubblicazioni consigliate
I metadati presenti in IRIS UNIMORE sono rilasciati con licenza Creative Commons CC0 1.0 Universal, mentre i file delle pubblicazioni sono rilasciati con licenza Attribuzione 4.0 Internazionale (CC BY 4.0), salvo diversa indicazione.
In caso di violazione di copyright, contattare Supporto Iris
