A linear time algorithm for unique Horn satisfiability

Pretolani, Daniele

doi:10.1016/0020-0190(93)90178-C

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.

Attenzione! Scheda prodotto non ancora validata dall'Ateneo

Dati e metadati della pubblicazione sono in fase di verifica da parte dell'Ateneo. In caso di errori o violazione dei diritti d'autore, contattare: supporto.iris@unimore.it

Anno di pubblicazione:	1993
Titolo:	A linear time algorithm for unique Horn satisfiability
Autori:	D. PRETOLANI
Autori:	PRETOLANI, Daniele
Digital Object Identifier (DOI):	10.1016/0020-0190(93)90178-C
Rivista:	INFORMATION PROCESSING LETTERS
Volume:	48 (2)
Pagina iniziale:	61
Pagina finale:	66
Appare nelle tipologie:	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

Citazioni

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