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.
Data di pubblicazione: | 1993 |
Titolo: | A linear time algorithm for unique Horn satisfiability |
Autore/i: | Pretolani, Daniele |
Autore/i UNIMORE: | |
Digital Object Identifier (DOI): | http://dx.doi.org/10.1016/0020-0190(93)90178-C |
Rivista: | |
Volume: | 48 (2) |
Pagina iniziale: | 61 |
Pagina finale: | 66 |
Codice identificativo ISI: | WOS:A1993MH81800002 |
Codice identificativo Scopus: | 2-s2.0-0027912458 |
Citazione: | A linear time algorithm for unique Horn satisfiability / Pretolani, Daniele. - In: INFORMATION PROCESSING LETTERS. - ISSN 0020-0190. - STAMPA. - 48 (2)(1993), pp. 61-66. |
Tipologia | Articolo su rivista |
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti presenti in Iris Unimore sono rilasciati con licenza Creative Commons Attribuzione - Non commerciale - Non opere derivate 3.0 Italia, salvo diversa indicazione.
In caso di violazione di copyright, contattare Supporto Iris