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.
Rappresentazione del problema
Un'istanza di 2SAT può essere descritta utilizzando un'espressione booleana in forma normale congiuntiva, ovvero una congiunzione (l'operatore booleano e) di clausole, in cui ogni clausola è una disgiunzione (l'operatore booleano o) di due letterali. Ad esempio, la seguente formula è in forma normale congiuntiva, con 7 variabili, 11 clausole e 22 letterali:
Il problema 2SAT consiste nel trovare un'assegnazione di verità a queste variabili che renda vera l'intera formula. Tale assegnazione sceglie se rendere vera o falsa ciascuna delle variabili, in modo che almeno un letterale in ogni clausola sia vero. Per l'espressione mostrata sopra, una possibile assegnazione soddisfacente è quella che rende tutte e sette le variabili vere. Ogni clausola ha almeno un letterale positivo, quindi questa assegnazione soddisfa ogni clausola. Ci sono altri 15 modi per impostare le variabili in modo che la formula risulti vera. Pertanto, l'istanza di 2SAT rappresentata da questa espressione è soddisfacibile.
Le formule in questa forma sono conosciute come formule 2-CNF. Il "2" in questo nome sta per il numero di letterali per clausola e "CNF" sta per forma normale congiuntiva, un tipo di espressione booleana nella forma di congiunzione di disgiunzioni. Sono anche chiamate formule di Krom, dal lavoro del matematico della UC Davis Melven R. Krom, il cui articolo del 1967 è stato uno dei primi lavori sul problema della soddisfacibilità 2.
Ogni clausola in una formula 2-CNF è logicamente equivalente a un'implicazione da un letterale all'altro. Ad esempio, la seconda clausola nell'esempio può essere scritta in uno dei tre modi equivalenti:A causa dell'equivalenza tra questi diversi tipi di operazione, un'istanza di 2SAT può anche essere scritta in forma normale implicativa, in cui sostituiamo ciascuna clausola nella forma normale congiuntiva con le due implicazioni a cui è equivalente.
Un terzo modo più grafico per descrivere un'istanza di 2SAT è usando un grafo delle implicazioni. Un grafo delle implicazioni è un grafo orientato in cui c'è un vertice per ogni letterale e un arco che collega un vertice all'altro ogni volta che i corrispondenti letterali sono vincolati da un'implicazione nella forma normale implicativa dell'istanza. Ogni grafo delle implicazioni è un grafo skew-simmetrico, il che significa che il grafo ottenuto sostituendo ogni letterale con la sua negazione e invertendo gli orientamenti di tutti gli archi è isomorfo al grafo iniziale. Questa proprietà deriva dal fatto che ogni implicazione è rappresentata nel grafo sia da essa stessa, che dalla sua forma contronominale.
Algoritmo per la risoluzione del problema 2SAT Sono noti diversi algoritmi per risolvere il problema 2SAT. I più efficienti richiedono tempo lineare.
Aspvall, Plass e Tarjan (1979) hanno trovato una procedura lineare in tempo per risolvere istanze di 2SAT, basata sulla nozione di componenti fortemente connesse dalla teoria dei grafi.
Si dice che due vertici in un grafo diretto sono fortemente connessi tra loro se esiste un cammino dall'uno all'altro e viceversa. Questa è una relazione di equivalenza e i vertici del grafo possono essere partizionati in componenti fortemente connesse, sottoinsiemi all'interno dei quali ogni coppia di vertici è fortemente connessa. Esistono diversi algoritmi lineari in tempo per trovare le componenti fortemente connesse di un grafo, basati sulla ricerca in profondità: l'algoritmo di Tarjan e l'algoritmo basato sui cammini eseguono una singola ricerca in profondità. L'algoritmo di Kosaraju esegue due ricerche in profondità, ma è molto semplice.
In termini di grafo delle implicazioni, due letterali appartengono alla stessa componente fortemente connessa ogni volta che esiste una catena di implicazioni da un letterale all'altro e viceversa. Pertanto, i due letterali devono avere lo stesso valore in qualsiasi assegnazione soddisfacente l'istanza data. In particolare, se una variabile e la sua negazione appartengono entrambe alla stessa componente fortemente connessa, l'istanza non è soddisfacibile, perché è impossibile assegnare a entrambi i letterali lo stesso valore. Come Aspvall et al. hanno dimostrato, questa è una condizione necessaria e sufficiente: una formula 2-CNF è soddisfacibile se e solo se nessuna variabile appartiene alla stessa componente fortemente connessa a cui appartiene la sua negazione.
Ciò porta immediatamente a un algoritmo lineare per testare la soddisfacibilità delle formule 2-CNF: è sufficiente eseguire un'analisi della connettività forte sul grafo delle implicazioni e verificare che ogni variabile e la sua negazione appartengano a componenti diverse. Inoltre, come Aspvall et al. hanno provato, questo algoritmo trova anche un'assegnazione soddisfacente, quando esiste. L'algoritmo è descritto attraverso i seguenti passi:
Costruisci il grafo delle implicazioni dell'istanza e trova le componenti fortemente connesse utilizzando uno qualsiasi degli algoritmi lineari per l'analisi di connettività forte. Controlla se una componente fortemente connessa contiene sia una variabile che la sua negazione. In tal caso, l'istanza non è soddisfacibile e l'algoritmo termina. Costruisci la condensazione del grafo, un grafo più piccolo che ha un vertice per ogni componente fortemente connessa e un arco dalla componente alla componente ogni volta che il grafo delle implicazioni contiene un arco tale che appartenga alla componente e appartenga alla componente . La condensazione è automaticamente un grafo aciclico orientato e, come il grafo da cui è stato formato, è skew-simmetrico. Ordina topologicamente i vertici della condensazione. In pratica, ciò può essere ottenuto in modo efficiente come effetto collaterale del passo 1, poiché le componenti sono generate dall'algoritmo di Kosaraju in ordine topologico e dall'algoritmo di Tarjan in ordine topologico inverso. Per ogni componente in ordine topologico inverso, se i suoi elementi non hanno già valori di verità assegnati, poni tutti letterali della componente veri. Ciò fa sì che tutti i letterali della componente duale vengano posti falsi.
A causa dell'ordinamento topologico inverso e della skew-simmetria del grafo, quando un letterale è posto vero, tutti i letterali che possono essere raggiunti da esso tramite una catena di implicazioni saranno già stati posti veri. Simmetricamente, quando un letterale è posto falso, tutti i letterali che portano ad esso attraverso una catena di implicazioni saranno già stati posti falsi. Pertanto, l'assegnazione di verità costruita da questa procedura soddisfa la formula data, che completa anche la prova di correttezza della condizione necessaria e sufficiente individuata da Aspvall et al.
Come Aspvall et al. hanno dimostrato, una procedura simile che coinvolge l'ordinamento topologico delle componenti fortemente connesse del grafo delle implicazioni può essere utilizzata per valutare le formule booleane completamente quantificate in cui la formula che viene quantificata è una formula 2-CNF.
Pseudocodice Un modo efficiente di implementare l'algoritmo sta nel seguente pseudocodice:
algorithm Aspvall-Plass-Tarjan input: una formula booleana 2-CNF F = (a_1 ∨ b_1) ∧ ... ∧ (a_n ∨ b_n) output: un'assegnazione di verità T tale che T(F) = true, se esiste, altrimenti null
G := implicationGraph() T := [1, ..., |G.V|] // contatore del numero di nodi index := 1 // La pila dei nodi, inizialmente vuota S := []
// avvia la ricerca depth-first per ogni nodo, finché non si trova una contraddizione i := 1 while i ≤ |G.V| and T ≠ null do v := G.V[i] if v.index = null then // il nodo non è stato ancora visitato computeAssignment(v) end if i := i + 1 end while
return T
// costruzione del grafo delle implicazioni function implicationGraph() G.V := [] G.A := []
for i := 1 to n do // aggiungi i letterali della clausola i-esima e i loro complementi ai nodi del grafo G.V.add(a_i) G.V.add(b_i) G.V.add(not(a_i)) G.V.add(not(b_i))
// aggiungi le implicazioni ¬a_i → b_i e ¬b_i → a_i agli archi del grafo G.A.add(<not(a_i), b_i>) G.A.add(<not(b_i), a_i>) end for
return G end function
function computeAssignment(v) // assegna a v l'indice attuale v.index := index v.lowlink := index index := index + 1 // aggiungi v alla pila S S.push(v)
// analizza i successori di v nel grafo finché la CFC corrente non assume un valore di verità for w in G.Adj[v] do if w.index = null and T[w] = null then // w non è stato ancora visitato e non ha un valore di verità; visitalo ricorsivamente computeAssignment(w) // se T è null, la formula è insoddisfacibile, ferma la ricerca if T = null then return end if v.lowlink := min(v.lowlink, w.lowlink) else if T[w] = null then // w è stato già visitato e non ha un valore di verità, dunque è nella CFC corrente