Back قابلية الإرضاء الثنائية Arabic 2-satisfiability English 2-satisfactibilidad Spanish Problème 2-SAT French
In informatica, 2-satisfiability, 2-SAT o semplicemente 2SAT è un problema di soddisfacibilità booleana con clausole composte da coppie di letterali. È un caso particolare (il più semplice) del problema n-SAT, ed è l'unico di cui è stata dimostrata la risolubilità in tempo polinomiale e spazio logaritmico. Più precisamente, si tratta di un problema NL-completo. Al contrario, i problemi di soddisfacibilità con sono tutti NP-completi, essendo tali sia il generico SAT (per il teorema di Cook) che 3-SAT (poiché ogni problema n-SAT è riducibile a 3-SAT in tempo polinomiale).
Le istanze di 2SAT sono tipicamente espresse come formule booleane di tipo particolare, dette in forma normale congiuntiva (2-CNF) o formule di Krom. In alternativa, possono essere espresse attraverso un grafo diretto, detto grafo delle implicazioni, in cui i letterali di un'istanza sono rappresentati dai vertici, e le clausole dagli archi diretti. Entrambi i tipi di istanze possono essere risolti in tempo lineare, sia con un metodo basato sul backtracking, sia utilizzando le componenti fortemente connesse del grafo delle implicazioni. La risoluzione, un metodo che combina coppie di clausole per creare ulteriori clausole valide, risolve il problema in tempo quadratico. 2SAT fornisce una delle due principali sottoclassi delle formule in CNF che possono essere risolte in tempo polinomiale, l'altra sottoclasse è la Horn-soddisfacibilità.
2SAT può essere applicato a problemi di geometria e di visualizzazione, in cui ciascun oggetto ha due possibili posizioni e l'obiettivo è trovare una posizione per ciascun oggetto che eviti sovrapposizioni con gli altri. Altre applicazioni includono il raggruppamento dei dati per ridurre al minimo la somma dei diametri dei cluster, la pianificazione delle classi e dei tornei e il riconoscimento delle forme dalle informazioni sulle loro sezioni trasversali.
Nella teoria della complessità computazionale, 2SAT fornisce un esempio di problema NL-completo, che può essere risolto in modo non deterministico utilizzando una quantità di memoria logaritmica, e che è tra i problemi più difficili risolvibili con questi limiti sulle risorse. All'insieme di tutte le soluzioni per un'istanza di 2SAT può essere data la struttura di un grafo mediano, ma il conteggio di queste soluzioni è #P-completo, quindi non ci si aspetta che abbia una soluzione in tempo polinomiale. Le istanze casuali subiscono una netta transizione di fase da istanze risolvibili a istanze irrisolvibili quando il rapporto tra clausole e variabili aumenta oltre 1, un fenomeno ipotizzato ma non dimostrato per forme più complicate del problema di soddisfacibilità. Una variante computazionalmente difficile di 2SAT, trovare un'assegnazione di verità che massimizza il numero di clausole soddisfatte, ha un algoritmo di approssimazione la cui ottimalità dipende dalla congettura dei giochi unici; un'altra variante difficile, trovare un'assegnazione soddisfacente che riduce al minimo il numero di variabili vere, è un importante caso di test per la complessità parametrizzata.