2-satisfiability

Questa voce o sezione sull'argomento matematica è ritenuta da controllare.

Motivo: "solita" traduzione semiautomatica in cui le fonti non sono state riportate correttamente dalla versione di origine

---

Partecipa alla discussione e/o correggi la voce. Segui i suggerimenti del progetto di riferimento.

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 ${\displaystyle n>2}$ 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.

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.^[1] Ad esempio, la seguente formula è in forma normale congiuntiva, con 7 variabili, 11 clausole e 22 letterali:

${\displaystyle {\begin{aligned}&(x_{0}\lor x_{2})\land (x_{0}\lor \neg x_{3})\land (x_{1}\lor \neg x_{3})\land (x_{1}\lor \neg x_{4})\land \\&(x_{2}\lor \neg x_{4})\land (x_{0}\lor \neg x_{5})\land (x_{1}\lor \neg x_{5})\land (x_{2}\lor \neg x_{5})\land \\&(x_{3}\lor x_{6})\land (x_{4}\lor x_{6})\land (x_{5}\lor x_{6})\end{aligned}}}$

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.^[1] 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.^[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:$${\displaystyle (x_{0}\lor \neg x_{3})\ \equiv \ (\lnot x_{0}\to \neg x_{3})\ \equiv \ (x_{3}\to x_{0})}$$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.^[3]

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.^[4] Questa proprietà deriva dal fatto che ogni implicazione è rappresentata nel grafo sia da essa stessa, che dalla sua forma contronominale.

Sono noti diversi algoritmi per risolvere il problema 2SAT. I più efficienti richiedono tempo lineare.^[4][5][6]

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.^[4]

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^[7] 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.^[4]

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 ${\displaystyle i}$ alla componente ${\displaystyle j}$ ogni volta che il grafo delle implicazioni contiene un arco ${\displaystyle (u,v)}$ tale che ${\displaystyle u}$ appartenga alla componente ${\displaystyle i}$ e ${\displaystyle v}$ appartenga alla componente ${\displaystyle j}$. 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.^[8]
• 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.^[4]

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.^[4]

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à
        j := 1
        while j ≤ G.Adj[v].length and T[v] = null do
            w := G.Adj[v][j]
            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
                // Se w ha un valore di verità, allora (v, w) è un arco che punta ad una CFC già riconosciuta e va ignorato
                v.lowlink := min(v.lowlink, w.index) // w è in S ma non nel sotto-ramo ottenuto nella ricerca depth-first
            end if
            j := j + 1
        end while

        // Se v è la radice di un sottoalbero, esso forma una CFC, pertanto dev'essere tolta dallo stack
        if v.lowlink = v.index then
            if T[v] ≠ null then
                // è già stato assegnato un valore di verità alla CFC, ci limitiamo solo toglierla dallo stack
                repeat
                    w := S.pop()
                while w ≠ v
            else
                // togliamo la CFC dallo stack, assegniamo true alla CFC e false al suo duale
                repeat
                    w := S.pop()

                    // se w ha già un valore di verità, allora il suo complemento è nella CFC, per cui la formula è insoddisfacibile
                    if T[w] ≠ null then
                        T := null
                        return
                    end if

                    // assegna true a w e false al suo complemento
                    T[w] := true
                    T[not(w)] := false
                while w ≠ v
            end if
        end if
    end function

Un certo numero di algoritmi esatti e approssimativi per il problema del posizionamento automatico delle etichette si basano su 2SAT. Questo problema riguarda l'inserimento di etichette testuali sulle caratteristiche di un diagramma o di una mappa. Tipicamente, l'insieme delle possibili posizioni per ciascuna etichetta è fortemente vincolato, non solo dalla mappa stessa (ogni etichetta deve essere vicina alla caratteristica che etichetta e non deve oscurare altre caratteristiche), ma l'una dall'altra: ogni coppia di etichette dovrebbe evitare la sovrapposizione l'un l'altra, perché altrimenti diventerebbero illeggibili. In generale, trovare un posizionamento dell'etichetta che obbedisca a questi vincoli è un problema NP-difficile. Tuttavia, se ogni feature ha solo due possibili posizioni per la sua etichetta (ad esempio, a sinistra e a destra della feature), il posizionamento dell'etichetta può essere risolto in tempo polinomiale. Perché, in questo caso, si può creare un'istanza di 2SAT che ha un certo numero di variabili per ciascuna etichetta e che ha una clausola per ciascuna coppia di etichette che potrebbero sovrapporsi, impedendo loro di essere assegnate a posizioni sovrapposte. Se le etichette sono tutti rettangoli congruenti, è possibile dimostrare che la lunghezza dell'istanza di 2SAT corrispondente è lineare, portando ad algoritmi quasi lineari in tempo per trovare un'etichettatura.^[9] Poon, Zhu e Chin descrivono un problema di etichettatura della mappa in cui ogni etichetta è un rettangolo che può essere posizionato in una delle tre posizioni rispetto a un segmento di retta etichettato: il segmento può essere uno dei suoi lati, oppure può essere centrata sul segmento. Rappresentano queste tre posizioni utilizzando due variabili binarie, in modo tale che verificare l'esistenza di un'etichettatura valida diventi un'istanza di 2SAT.^[10]

Formann e Wagner (1991) utilizzano 2SAT come parte di un algoritmo di approssimazione per il problema di trovare etichette quadrate di dimensione più grande possibile per un dato insieme di punti, con il vincolo che ogni etichetta abbia uno dei suoi angoli nel punto che etichetta. Per trovare un'etichettatura di una data dimensione, eliminano i quadrati che, se raddoppiati, si sovrapporrebbero a un altro punto ed eliminano i punti che possono essere etichettati in un modo che non possa sovrapporsi all'etichetta di un altro punto. Mostrano che queste regole di eliminazione fanno sì che i punti rimanenti abbiano solo due possibili posizionamenti di etichette per punto, consentendo di trovare un posizionamento di etichette valido (se esistente) come soluzione a un'istanza di 2SAT. Cercando la più grande dimensione delle etichette che porta a un'istanza di 2SAT risolvibile, trovano un posizionamento valido, le cui etichette sono grandi almeno la metà della soluzione ottimale. Cioè, il rapporto di approssimazione del loro algoritmo è al massimo due.^[11][12] Allo stesso modo, se ogni etichetta è rettangolare e deve essere posizionata in modo tale che il punto che etichetta sia da qualche parte lungo il bordo inferiore, utilizzare 2SAT per trovare la più grande dimensione delle etichette per la quale esiste una soluzione in cui ogni etichetta ha il suo punto su un angolo inferiore porta a un rapporto di approssimazione di al massimo due.^[13]

Applicazioni simili di 2SAT sono state scoperte per altri problemi di posizionamento geometrico. Nel disegno grafico, se le posizioni dei vertici sono fisse e ogni spigolo deve essere disegnato come un arco circolare con due possibili posizioni (ad esempio come diagramma ad arco), allora il problema di scegliere quale arco usare per ogni spigolo per evitare incroci è un'istanza di 2SAT con una variabile per ciascun bordo e un vincolo per ciascuna coppia di posizionamenti che porterebbero a un incrocio. Tuttavia, in questo caso è possibile velocizzare la soluzione, rispetto ad un algoritmo che costruisce e poi ricerca una rappresentazione esplicita del grafo delle implicazioni, ricercando il grafo implicitamente.^[14] Nella progettazione di circuiti integrati VLSI, se un insieme di moduli deve essere collegato mediante fili che possono piegarsi ciascuno al massimo una volta, anche in questo caso ci sono due possibili percorsi per i fili, e il problema di scegliere quale di questi due percorsi utilizzare, in un modo tale che tutti i fili possano essere instradati in un singolo strato del circuito, può essere risolto come un'istanza di 2SAT.^[15]

Boro e altri (1999) considerano un altro problema di progettazione VLSI: la questione se invertire o meno ogni modulo in un progetto di circuito. Questa inversione speculare lascia invariate le operazioni del modulo, ma cambia l'ordine dei punti in cui i segnali di ingresso e di uscita del modulo si collegano ad esso, modificando eventualmente il modo in cui il modulo si adatta al resto del progetto. Essi considerano una versione semplificata del problema in cui i moduli sono già stati posizionati lungo un unico canale lineare, in cui i fili tra i moduli devono essere instradati, e c'è un limite fisso sulla densità del canale (il numero massimo di segnali che deve attraversare qualsiasi sezione del canale). Osservano che questa versione del problema può essere risolta come un'istanza 2SAT, in cui i vincoli mettono in relazione gli orientamenti di coppie di moduli, in cui uno si trova direttamente dall'altra parte del canale rispetto all'altro. Di conseguenza, la densità ottimale può anche essere calcolata in modo efficiente, eseguendo una ricerca binaria in cui ogni passaggio implica la soluzione di un'istanza 2SAT.^[16]

Un modo per raggruppare un insieme di punti di dati in uno spazio metrico in due cluster è scegliere i cluster in modo tale da ridurre al minimo la somma dei diametri dei cluster, dove il diametro di ogni singolo cluster è la massima distanza tra le coppie dei suoi punti. Ciò è preferibile alla minimizzazione della dimensione massima dei cluster, che può comportare l'assegnazione di punti molto simili a cluster diversi. Se i diametri target dei due cluster sono noti, è possibile trovare un clustering che realizza tali target risolvendo un'istanza di 2SAT. L'istanza ha una variabile per punto, che indica se quel punto appartiene al primo o al secondo cluster. Ogni volta che due punti sono troppo distanti l'uno dall'altro perché entrambi appartengano allo stesso cluster, all'istanza viene aggiunta una clausola che impedisce questa assegnazione.

Lo stesso metodo può essere utilizzato anche come subroutine quando i diametri dei singoli cluster sono sconosciuti. Per verificare se una data somma di diametri può essere raggiunta senza conoscere i singoli diametri del cluster, si possono provare tutte le coppie massimali di diametri target che, se sommate, danno come risultato al più la somma data, rappresentando ciascuna coppia di diametri come un'istanza di 2SAT e utilizzando un algoritmo 2SAT per determinare se quella coppia può essere realizzata da un clustering. Per trovare la somma ottimale dei diametri si può effettuare una ricerca binaria, in cui ogni passaggio è un test di realizzabilità di questo tipo. Lo stesso approccio funziona anche per trovare raggruppamenti che ottimizzino combinazioni diverse dalle somme dei diametri dei cluster e che utilizzino valori di differenza arbitrari (piuttosto che le distanze in uno spazio metrico) per misurare le dimensioni di un cluster.^[17] Il tempo di esecuzione per questo algoritmo è minore o uguale al tempo necessario per risolvere una sequenza di istanze 2SAT strettamente correlate tra loro; Ramnath mostra come risolvere queste istanze più rapidamente che se fossero risolte indipendentemente l'una dall'altra, portando il tempo di esecuzione a O(n³) per il problema del clustering della somma dei diametri.^[18]

Even, Itai e Shamir (1976) considerano un modello di organizzazione delle classi in cui dev'essere pianificato l'insegnamento di un insieme di n insegnanti a ciascuna delle m classi di studenti. Il numero di ore settimanali in cui l'insegnante ${\displaystyle i}$ insegna nella classe ${\displaystyle j}$ è indicato dall'elemento ${\displaystyle R_{ij}}$ di una matrice ${\displaystyle R}$, data come input del problema, e ogni insegnante ha una serie di ore di disponibilità all'insegnamento. Come dimostrano, il problema è NP-completo, anche quando ogni insegnante ha al massimo tre ore disponibili, ma può essere risolto come un'istanza di 2SAT quando ogni insegnante ha solo due ore disponibili (gli insegnanti con una sola ora disponibile possono essere facilmente eliminati dal problema). In questo problema, ogni variabile ${\displaystyle v_{ij}}$ corrisponde a un'ora in cui l'insegnante ${\displaystyle i}$ deve insegnare alla classe ${\displaystyle j}$, il valore della variabile specifica se quell'ora è la prima o la seconda delle ore disponibili del docente, e c'è una clausola di 2 letterali che impedisce un qualsiasi conflitto di questi due tipi: un insegnante assegnato a due classi alla stessa ora o una classe assegnata a due insegnanti alla stessa ora.^[6]

Miyashiro e Matsui (2005) applicano 2SAT ad un problema di programmazione di partite, in cui sono già stati scelti gli accoppiamenti di un girone all'italiana e le partite devono essere assegnate agli stadi delle squadre. In questo problema, è auspicabile alternare per quanto possibile le partite in casa e quelle in trasferta, evitando "interruzioni" in cui una squadra gioca due partite casalinghe di fila o due partite in trasferta di fila. Al massimo due squadre possono evitare del tutto le interruzioni, alternando partite in casa e in trasferta; nessun'altra squadra può avere la stessa programmazione casa-trasferta di queste due, perché in tal caso non potrebbe giocare con la squadra con cui avrebbe la stessa programmazione. Pertanto, una programmazione ottimale prevede due squadre senza interruzioni e una singola interruzione per ogni altra squadra. Una volta scelta una delle squadre senza interruzioni, è possibile impostare un'istanza 2SAT in cui ogni variabile rappresenta l'assegnazione casa-trasferta di una singola squadra in una singola partita e i vincoli impongono le proprietà che due squadre qualsiasi hanno un'assegnazione coerente per le loro partite, che ogni squadra abbia al più un'interruzione prima e al più un'interruzione dopo la partita con la squadra senza interruzioni e che nessuna squadra abbia due interruzioni. Pertanto, è possibile verificare se un girone ammette una soluzione con il numero ottimale di interruzioni risolvendo una quantità lineare di istanze 2SAT, una per ogni scelta della squadra senza interruzioni. Una tecnica simile consente di trovare programmazioni in cui ogni squadra ha una singola interruzione e di massimizzare anziché ridurre al minimo le interruzioni (per ridurre i chilometri totali percorsi dalle squadre).^[19]

La tomografia è il processo di recupero delle forme dalle loro sezioni trasversali. Nella tomografia discreta, una versione semplificata del problema che è stato frequentemente studiato, la forma da recuperare è un polimino (un sottoinsieme dei quadrati nel reticolo quadrato bidimensionale), e le sezioni trasversali forniscono informazioni aggregate sugli insiemi di quadrati nelle singole righe e colonne del reticolo. Ad esempio, nei popolari puzzle nonogrammi, noti anche come "dipingi con i numeri" o "griddlers", i quadrati da determinare rappresentano i pixel scuri in un'immagine binaria e l'input dato al risolutore di puzzle dichiara quanti blocchi consecutivi di pixel scuri vanno inclusi in ogni riga o colonna dell'immagine e quanto dovrebbe essere lungo ciascuno di questi blocchi. In altre forme di tomografia digitale, vengono fornite ancora meno informazioni su ogni riga o colonna: solo il numero totale di quadrati, invece che il numero e la lunghezza dei blocchi di quadrati. Una versione equivalente del problema sta nel recuperare una matrice binaria, data solo la somma dei valori in ogni riga e in ogni colonna della matrice.

Sebbene esistano algoritmi polinomiali per trovare una matrice data la somma dei valori in ogni riga e colonna,^[20] la soluzione può non essere unica: qualsiasi sottomatrice nella forma di una matrice identità 2×2 può essere complementata senza compromettere la correttezza della soluzione. Pertanto, i ricercatori hanno cercato vincoli sulla forma da ricostruire che possono essere utilizzati per limitare lo spazio delle soluzioni. Ad esempio, si potrebbe presumere che la forma sia connessa; tuttavia, verificare se esiste una soluzione connessa è un problema NP-completo.^[21] Una versione ancora più vincolata che è più facile da risolvere è l'esistenza di una forma ortogonalmente convessa, avendo un unico blocco contiguo di quadrati in ogni riga e colonna. Migliorando diverse soluzioni precedenti, Chrobak e Dürr (1999) hanno mostrato come ricostruire in modo efficiente forme connesse ortogonalmente convesse, utilizzando 2SAT.^[22] L'idea della loro soluzione è di indovinare gli indici delle righe contenenti le celle più a sinistra e più a destra della forma da ricostruire, e quindi impostare un'istanza 2SAT che verifichi se esiste una forma coerente con queste ipotesi e con la somma dei valori in ogni riga e colonna. Usano quattro variabili binarie per ogni quadrato che potrebbe far parte della forma, ciascuna per indicare se appartiene a una delle quattro possibili "regioni angolari" della forma, e usano vincoli che costringono queste regioni a essere disgiunte, per avere le forme desiderate, in modo da creare una forma complessiva con righe e colonne contigue e per avere le somme dei valori desiderate in ogni riga e colonna. Il loro algoritmo richiede un tempo di esecuzione O(m³n), dove m è la minore tra le due dimensioni dell'input e n è la maggiore. Lo stesso metodo è stato esteso successivamente a forme ortogonalmente convesse che possono essere connesse solo in diagonale, invece che esserlo ortogonalmente.^[23][24][25]

In una parte di un risolutore di nonogrammi completi, Batenburg e Kosters (2008, 2009) hanno utilizzato 2SAT per combinare le informazioni ottenute da diverse altre euristiche. Data una soluzione parziale del puzzle, usano la programmazione dinamica all'interno di ogni riga o colonna per determinare se i vincoli di quella riga o colonna costringono uno qualsiasi dei suoi quadrati a essere bianco o nero e se due quadrati nella stessa riga o colonna possono essere collegati da una relazione di implicazione. Inoltre, trasformano il nonogramma in un problema di tomografia digitale sostituendo la sequenza delle lunghezze dei blocchi in ogni riga e colonna con la loro somma, e utilizzano una formulazione del problema di flusso massimo per determinare, combinando tutte le righe e le colonne, se questo problema di tomografia digitale ha dei quadrati il cui stato può essere determinato o coppie di quadrati che possono essere collegati da una relazione di implicazione. Se una di queste due euristiche determina il valore di uno dei quadrati, viene incluso nella soluzione parziale e vengono ripetuti gli stessi calcoli. Tuttavia, se entrambe le euristiche non riescono a ricavare il valore di un quadrato, le implicazioni trovate da entrambe vengono combinate in un'istanza 2SAT e viene utilizzato un risolutore 2SAT per trovare quadrati il cui valore è fissato dall'istanza, dopodiché la procedura è ripetuta ancora. Questa procedura può non riuscire a trovare una soluzione, ma è garantita l'esecuzione in tempo polinomiale. Batenburg e Kosters riferiscono che, sebbene la maggior parte degli enigmi sui giornali non richieda la loro piena potenza, sia questa procedura sia una procedura più potente ma più lenta, che combina questo approccio di 2SAT con il backtracking limitato di Even, Itai e Shamir (1976)^[26], sono significativamente più efficaci della programmazione dinamica e dell'euristica del flusso senza 2SAT se applicate a nonogrammi più difficili generati casualmente.^[27][28]

Accanto a 2SAT, l'altra principale sottoclasse di problemi di soddisfacibilità che possono essere risolti in tempo polinomiale è la Horn-soddisfacibilità. In questo tipo di problemi di soddisfacibilità, l'input è sempre una formula in forma normale congiuntiva. Può avere un numero arbitrario di letterali per clausola, ma al più un letterale positivo. Lewis (1978) ha trovato una generalizzazione di questa classe, soddisfacibilità di Horn rinominabile, che può ancora essere risolta in tempo polinomiale per mezzo di un'istanza ausiliaria di 2SAT. Una formula è Horn-rinominabile quando è possibile tradurla nella forma di Horn sostituendo alcune variabili con le loro negazioni. Per fare ciò, Lewis imposta un'istanza 2SAT con una variabile per ciascuna variabile dell'istanza Horn-rinominabile, in cui le variabili dell'istanza 2SAT indicano se negare o meno le corrispondenti variabili dell'istanza Horn-rinominabile. Per produrre un'istanza nella forma di Horn, nessuna coppia di variabili che occorrono nella stessa clausola dell'istanza Horn-rinominabile dovrebbero comparire positivamente in quella clausola; questo vincolo su coppie di variabili è una clausola 2SAT. Trovando un'assegnazione soddisfacente all'istanza 2SAT risultante, Lewis mostra come trasformare qualsiasi istanza Horn-rinominabile in un'istanza nella forma di Horn in tempo polinomiale.^[29] Spezzando le clausole lunghe in clausole più piccole e applicando un algoritmo 2SAT in tempo lineare, è possibile ridurre la complessità a tempo lineare.^[30]

2SAT è stato applicato anche a problemi di riconoscimento di grafi non orientati che possono essere partizionati in un insieme indipendente e in un piccolo numero di sottografi bipartiti completi,^[31] deduzione di relazioni commerciali tra sottosistemi autonomi di Internet^[32][33] e ricostruzione di alberi filogenetici.^[34]

Un algoritmo non deterministico per determinare se un'istanza 2SAT non è soddisfacibile, utilizzando solo una quantità logaritmica di memoria, è facile da descrivere: scegli (in modo non deterministico) una variabile v e cerca (in modo non deterministico) una catena di implicazioni da v alla sua negazione e poi dalla sua negazione a v. Se questa catena esiste, l'istanza è insoddisfacibile. Per il teorema di Immerman-Szelepcsényi, è possibile anche verificare in spazio logaritmico non deterministico che un'istanza 2SAT soddisfacibile è soddisfacibile.

2SAT è NL-completo,^[35] il che significa che è uno dei problemi "più difficili" o "più espressivi" nella classe di complessità NL dei problemi risolvibili non deterministicamente in spazio logaritmico. La completezza qui significa che una macchina di Turing deterministica che utilizza solo spazio logaritmico può trasformare ogni istanza di un qualsiasi altro problema in NL in un'istanza di 2SAT equivalente. Analogamente a risultati simili per la più nota classe di complessità NP, questa trasformazione insieme al teorema di Immerman-Szelepcsényi consente di rappresentare qualsiasi problema in NL come una formula logica del secondo ordine con un singolo predicato esistenzialmente quantificato e clausole di lunghezza 2. Tali formule sono conosciute come SO-Krom.^[36] Allo stesso modo, la forma normale implicativa può essere espressa in logica del primo ordine con l'aggiunta di un operatore per la chiusura transitiva.^[37]

L'insieme di tutte le soluzioni di un'istanza 2SAT ha la struttura di un grafo mediano, in cui ogni arco corrisponde all'operazione di negazione dei valori di un insieme di variabili che sono tutte vincolate a essere uguali o diverse a coppie. In particolare, seguendo gli archi si può passare da qualsiasi soluzione a qualsiasi altra soluzione. Al contrario, in questo modo qualsiasi grafo mediano può essere rappresentato come l'insieme delle soluzioni per un'istanza 2SAT. La mediana di tre soluzioni qualsiasi si ottiene impostando ciascuna variabile sul valore che assume nella maggioranza delle tre soluzioni. Questa mediana costituisce sempre un'ulteriore soluzione per l'istanza.^[38]

Feder (1994) descrive un algoritmo per elencare in modo efficiente tutte le soluzioni per una data istanza 2SAT e per risolvere diversi problemi correlati.^[39] Esistono anche algoritmi per trovare due assegnazioni soddisfacenti che hanno tra loro distanza di Hamming massima.^[40]

#2SAT è il problema di contare il numero di assegnazioni soddisfacenti per una data formula 2-CNF. Questo problema di conteggio è #P-completo^[41], il che implica che non è risolvibile in tempo polinomiale a meno che P = NP. Inoltre, non esiste uno schema di approssimazione randomizzato completamente polinomiale per #2SAT a meno che NP = RP e questo vale anche quando l'input è limitato a formule 2-CNF monotone, cioè formule 2-CNF in cui ogni letterale è un'occorrenza positiva di una variabile.^[42]

L'algoritmo più veloce conosciuto per calcolare il numero esatto di assegnazioni soddisfacenti per un'istanza 2SAT ha tempo di esecuzione ${\displaystyle O(1.2377^{n})}$.^[43][44][45]

Si può formare un'istanza 2SAT in modo casuale, per un dato numero n di variabili ed m di clausole, scegliendo ciascuna clausola in modo uniformemente casuale dall'insieme di tutte le possibili clausole a due letterali. Quando m è piccolo rispetto a n, tale istanza sarà probabilmente soddisfacibile, ma per valori maggiori di m, le istanze hanno minor probabilità di essere soddisfacibili. Più precisamente, se m / n è fissato come costante α ≠ 1, la probabilità di soddisfacibilità tende ad un limite per n che va ad infinito: se α < 1, il limite è 1, mentre se α > 1 il limite è 0. Pertanto, il problema mostra una transizione di fase per α = 1.^[46]

Nel problema maximum-2-satisfiability (MAX-2-SAT), l'input è un'istanza 2SAT e la richiesta è determinare il numero massimo di clausole che possono essere soddisfatte da un'assegnazione. Come il più generale problema di massima soddisfacibilità, MAX-2-SAT è NP-difficile. La prova è per riduzione di 3SAT.^[47]

Formulando MAX-2-SAT come il problema di trovare un taglio (cioè una partizione dei vertici in due sottoinsiemi) massimizzando il numero di archi che hanno un estremo nel primo sottoinsieme e l'altro estremo nel secondo, in un grafo correlato al grafo delle implicazioni, e applicando metodi di programmazione semidefinita a questo problema di taglio, è possibile trovare in tempo polinomiale una soluzione approssimativa che sia almeno 0.940... volte il numero massimo di clausole.^[48] Un'istanza di MAX-2-SAT bilanciata è un'istanza di MAX-2-SAT in cui ogni variabile appare positivamente e negativamente con lo stesso peso. Per questo problema, Austrin ha migliorato il rapporto di approssimazione a ${\displaystyle \min \left\{(3-\cos \theta )^{-1}(2+(2/\pi )\theta )\,:\,\pi /2\leq \theta \leq \pi \right\}=0.943...}$.^[49]

Se la congettura dei giochi unici è vera, allora è impossibile approssimare MAX-2-SAT, bilanciato o meno, con una costante di approssimazione migliore di 0,943... in tempo polinomiale.^[50] Sotto l'ipotesi più debole che P ≠ NP, il problema è noto solo per essere inapprossimabile al di sopra di una costante migliore di 21/22 = 0,95454...^[51]

Vari autori hanno anche esplorato i limiti di tempo esponenziali nel caso peggiore per la soluzione esatta delle istanze MAX-2-SAT.^[52]

Nel problema weighted-2-satisfiability (W2SAT), l'input è un'istanza 2SAT con ${\displaystyle n}$ variabili e un naturale ${\displaystyle k\leq n}$, la richiesta è decidere se esiste un'assegnazione soddisfacente in cui esattamente ${\displaystyle k}$ variabili sono vere.^[53]

Il problema W2SAT include come caso speciale il problema della copertura dei vertici, che consiste nel trovare ${\displaystyle k}$ vertici che insieme tocchino tutti gli archi di un dato grafo non orientato. Per ogni data istanza del problema della copertura dei vertici, si può costruire un problema W2SAT equivalente con una variabile per ogni vertice del grafo. Ciascun arco ${\displaystyle (u,v)}$ del grafo può essere rappresentato da una clausola ${\displaystyle u\lor v}$ che può essere soddisfatta solo includendo ${\displaystyle u}$ o ${\displaystyle v}$ tra le variabili vere della soluzione. Quindi, le assegnazioni soddisfacenti dell'istanza 2SAT risultante codificano soluzioni al problema della copertura dei vertici, e c'è un'assegnazione soddisfacente con ${\displaystyle k}$ variabili vere se e solo se esiste una copertura con ${\displaystyle k}$ vertici. Pertanto, come la copertura dei vertici, W2SAT è NP-completo.

Inoltre, nella complessità parametrizzata W2SAT fornisce un problema naturale W[1]-completo, il che implica che W2SAT non è trattabile a parametri fissi, a meno che ciò valga per tutti i problemi in W[1]. Cioè, è improbabile che esista un algoritmo per W2SAT il cui tempo di esecuzione assume la forma ${\displaystyle f(k)\cdot n^{O(1)}}$. In modo ancora più forte, W2SAT non può essere risolto in un tempo ${\displaystyle n^{O(k)}}$ a meno che l'ipotesi del tempo esponenziale sia falsa.^[54]

Oltre a trovare il primo algoritmo in tempo polinomiale per 2SAT, Krom (1967) ha anche formulato il problema della valutazione di formule booleane completamente quantificate, in cui la formula quantificata è in forma 2-CNF. 2SAT è un caso speciale di questo problema, in cui tutti i quantificatori sono esistenziali. Krom ha anche sviluppato una procedura di decisione effettiva per queste formule. Aspvall, Plass e Tarjan (1979) hanno dimostrato che può essere risolto in tempo lineare, mediante un'estensione della loro tecnica facente uso delle componenti fortemente connesse e dell'ordinamento topologico.^[2][4]

2SAT può anche essere esteso a logiche polivalenti. Gli algoritmi di solito non sono lineari e per alcune logiche il problema è addirittura NP-completo. Si veda Hähnle (2001, 2003)^[55] per gli studi a riguardo.

Portale Informatica

Portale Matematica