EnglishIn 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.
Utilizza questo identificativo per citare o creare un link a questo documento:
http://hdl.handle.net/11380/585408
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
Copyright © 2021