ASD2 - 01 - Algoritmi Greedy
Date:
Course Site:
Lecturer: Francesco Pasquale
Table of Contents:
In questa prima lezione abbiamo ripassato il paradigma greedy, discutendo un algoritmo in grado di risolvere il problema 3-SAT per particolare istanze, dette formule di horn.
Come primo algoritmo greedy andiamo a vedere un algoritmo che verifica la soddisfacibiltà di una formula di Horn. Iniziamo quindi con qualche definizione.
Definizione: Una clausola di Horn è una disgiunzione (\(\lor\)) di variabili, in cui al massimo una variabile appare positiva (non negata).
Se una clausola di Horn ha solo variabili negate, allora viene chiamata clausola di Horn negativa, altrimenti è detta clausola di Horn positiva.
Per fare un esempio, la clausola
\[(x_1 \lor x_2 \lor \neg x_3)\]
non è una clausola di horn, in quanto le variabili \(x_1\) e \(x_2\) sono entrambe positive. La clausola
\[(\neg x_2 \lor x_3)\]
invece è una clausola di horn (positiva). Anche la clausola
\[(x_1)\]
è una clausola di horn (positiva), in quanto contiene esattamente una sola variabile positiva.
A partire dal concetto di clausola di Horn possiamo introdurre il concetto di formula di Horn.
Definizione: Una formula di Horn è una congiunzione (\(\land\)) di clausole di Horn.
Dalla definizione segue che
\((\neg x_2 \lor x_3) \land (x_3)\) è una formula di Horn, mentre
\((x_1 \lor x_2 \lor \neg x_3) \land (x_1)\) non lo è.
Il problema che siamo interessati a risolvere è il solito problema di soddisfacibilità boolena per formule proposizionali, molto spesso chiamato 3SAT.
Il problema è così definito: Data una formula booleana in forma 3-CNF, ovvero formata da una congiunzione di clausole in cui ciascuna clausola è una disgiunzione di letterali, ci si chiede se esiste o meno una assegnazione di verità che soddisfa la formula.
Volendo formalizzare, sia \(I = \langle f, X \rangle\) una istanza di 3-SAT, con \(X = \{x_1, x_2, ..., x_n\}\) insieme delle variabili e \(f = C_1 \land ... \land C_2\) funzione booleana in 3-CNF, con \(C_i = ( l_{i,1} \lor l_{i, 2} \lor l_{i, 3})\) clausola di letterali. In altre parole,
\[f = (l_{1, 1} \lor l_{1, 2} \lor l_{1, 3}) \land (l_{2, 1} \lor l_{2, 2} \lor l_{2, 3}) \land ... \land (l_{m, 1} \lor l_{m, 2} \lor l_{m, 3})\]
È possibile dimostrare che il problema 3SAT è un problema NP-completo, il che significa che non è ancora stato trovato un modo efficiente (polinomiale) per risolvere tale problema. In questa lezione facciamo vedere come il problema diventa trattabile quando restringiamo l'insieme delle possibili istanze.
A tale fine definiamo il problema 3SAT-Horn, come il problema 3SAT in cui l'insieme delle istanze è ristretto all'insieme delle formule di Horn. Andiamo adesso a discutere un algoritmo che risolve in modo efficiente il problema 3SAT-Horn.
L'idea per risolvere il 3SAT-Horn è di risolvere il problema attraverso un algoritmo greedy. Gli algoritmi greedy sono algoritmi che, attraverso delle scelte locali ottimali, sono in grado di arrivare alla soluzione ottima.
Per il nostro particolare problema, per definire un algoritmo greedy ottimale possiamo giocare sul fatto che, dato che ogni clausola di Horn ha al massimo una variabile positiva, generalmente ci saranno più variabili negative che positive in ogni clausola.
Un possibile modo per iniziare è quindi quello di impostare a \(False\) tutte le variabili. Così facendo siamo sicuri di soddisfare tutte le clausole che contengono almeno una variabile negata. Notiamo però che questa assegnazione potrebbe non soddisfare la formula, in quanto ci potrebbero essere delle clausole che, ad esempio, sono formate solamente da una variabile positiva. Al fine di soddisfare tutte le clausole formate da una sola variabile positiva siamo quindi costretti ad impostare a \(True\) le suddette variabili. Questa scelta poi potrebbe non soddisfare una clausola che avevamo precedentemente soddisfatto. In questi casi quindi, al fine di soddisfare tale clausola, dobbiamo necessariamente impostare a \(True\) la variabile positiva contenuta nella clausola.
L'idea greedy dell'algoritmo è quindi quella di imposta le variabili a \(True\) solamente quando è strettamente necessario al fine di soddisfare la formula. Segue una descrizione dell'algoritmo
Prima di analizzare la correttezza e la complessità dell'algoritmo, andiamo a vedere un esempio di esecuzione. Sia \(\phi\) la seguente formula di Horn
\[\phi = (x_1 \lor \neg x_2 \lor \neg x_3) \land ( x_2 \lor \neg x_3) \land (x_3)\]
I passi che esegue l'algoritmo \(GreedyHorn\) sulla formula \(\phi\) in input sono i seguenti:
Si costruisce i due insiemi di clausole, l'insieme NEG contenente le clausole negative e l'insieme POS contenente le clausole positive. Nel nostro caso abbiamo
\[\begin{cases} \text{NEG} &= \emptyset \\ \text{POS} &= \{ (x_1 \lor \neg x_2 \lor \neg x_3), ( x_2 \lor \neg x_3), (x_3) \} \end{cases}\]
Imposta tutte le variabili (\(x_1\), \(x_2\), \(x_3\)) a \(False\);
Visto che esiste una clausola in POS non soddisfatta (la terza), la variabile positiva della clausola (\(x_3\)) viene impostata a \(True\), soddisfandola;
Nuovamente, visto che esiste una clausola in POS non soddisfatta (la seconda), la variabile positiva della clausola (\(x_2\)) viene impostata a \(True\), soddisfandola;
Si ripete nuovamente il passo precedente, impostando \(x_1\) a \(True\) e soddisfando la prima clausola;
Avendo soddisfatto tutte le clausole in POS, l'algoritmo controlla se anche tutte le clausole in NEG siano soddisfatte, e dato che lo sono, l'algoritmo termina, e l'assegnazione soddisfacente trovata è la seguente
\[\sigma (x_1) = \sigma (x_2) = \sigma (x_3) = True\]
Andiamo adesso ad argomentare la correttezza e la complessità dell'algoritmo.
Per quanto riguarda la correttezza, iniziamo notando che, se l'algoritmo ritorna un'assegnazione \(\sigma\), allora tale assegnazione, per costruzione, soddisfa sia POS che NEG, e quindi soddisfa \(\phi\). Se invece l'algoritmo ritorna \(None\), dobbiamo dimostrare che la formula \(\phi\) non può essere soddisfatta da nessuna assegnazione. Partiamo quindi dimostrando la seguente proposizione
Proposizione: Se, in una particolare iterazione del while loop eseguito dall'algoritmo, un insieme di variabili è impostato a \(True\), allora lo stesso insieme è impostato a \(True\) in ogni assegnazione di verità che soddisfa la formula.
Dimostrazione: La dimostrazione verrà fatta tramite l'induzione matematica sul numero di iterazioni \(t\) eseguite dal while loop
passo base: \((t = 1)\)
Alla prima iterazione del while loop tutte le variabili hanno il valore \(False\), quindi le uniche clausole in POS che non sono soddisfatte sono quelle composte da una singola variabile positiva \(x_i\). Ma allora, in ogni assegnazione che soddisfa la formula, questa variabile \(x_i\) deve necessariamente essere posta a \(True\), in quanto altrimenti la formula non può essere soddisfatta.
passo induttivo: \((t > 1)\)
Assumiamo, come ipotesi induttiva, che tutte le variabili poste a \(True\) nelle prime \(t\) iterazioni vengono poste a \(True\) in ogni assegnazione che soddisfa la formula e dimostriamo che questo vale anche per le variabili poste a \(True\) nella \((t+1)\) esima iterazione.
Sia \(y\) la variabile posta a true nella \((t+1)\) esima iterazione. Se \(y\) viene posta a \(True\), allora significa che \(y\) è l'unica variabile positiva di una clausola della forma \((\neg x_{i_1} \lor \neg x_{i_2} \lor ... \lor \neg x_{i_k} \lor y)\) in cui le variabili \(x_{i_j}\) sono state tutte poste a \(True\) in qualche iterazione precedente (se non fosse cosi, la clausola sarebbe soddisfatta da \(\sigma\) in questa iterazione, e quindi non verrebbe considerata). Ma allora, utilizzando l'ipotesi induttiva, abbiamo che le variabili \(x_{i_j}\) vengono poste a \(True\) da ogni assegnazione che soddisfa la formula. Nuovamente quindi, ogni assegnazione che soddisfa la formula, essendo costretta a porre a \(True\) tutte le variabili \(x_{i_j}\) della clausola in analisi, sarà anche costretta a mettere a \(True\) la variabile \(y\) se vuole soddisfare la formula \(\phi\).
\[\tag*{$\blacksquare$}\]
Andiamo adesso ad argomentare che la correttezza dell'algoritmo segue direttamente dalla proposizione appena dimostrata.
Dimostrazione: Sia \(\phi\) una formula tale che l'algoritmo GreedyHorn, con input \(\phi\), restituisce \(None\) e sia \(\sigma\) l'assegnazione costruita dall'algoritmo alla fine del while loop.
Supponiamo per assurdo che \(\phi\) sia soddisfacibile, ovvero che esiste una assegnazione \(\sigma^*\) che soddisfa \(\phi\). In altre parole, stiamo assumendo per assurdo che esiste un qualcosa che l'algoritmo non riesce a trovare.
Ora, come conseguenza diretta della proposizione, abbiamo che tutte le variabili che sono \(True\) per \(\sigma\), lo sono anche per \(\sigma^*\). Questo vuol dire che tutte le clausole in NEG che non sono soddisfatte da \(\sigma\), non sono soddisfatte nemmeno da \(\sigma^*\), in quanto potrebbero essere soddisfatte da \(\sigma^*\) solo se \(\sigma^*\) assegnasse \(False\) a una variabile che prende il valore \(True\) da \(\sigma\), ma tale scenario viene escluso dalla proposizione. Questo vuol dire quindi che, esistendo almeno una clausola in NEG non soddisfatta da \(\sigma\) (l'algoritmo ha ritornato \(None\)), allora questa clausola non è nemmeno soddisfatta da \(\sigma^*\), e quindi \(\sigma^*\) non soddisfa \(\phi\). Trovando un assurdo possiamo solo inferire che l'ipotesi che abbiamo fatto era sbagliata, e l'ipotesi fatta era che la formula \(\phi\) era soddisfacibile.
\[\tag*{$\blacksquare$}\]
La complessità dell'algoritmo è lineare, ovvero è un \(O(n)\).
Per implementare in modo efficiente l'algoritmo possono tornare utili le seguenti idee
Ad ogni clasuola è associato un punteggio. Questo punteggio varia durante l'esecuzione dell'algoritmo, ed è definito come il numero di variabili negate facenti parte della clausola che sono ancora settate a False in quel punto dell'esecuzione. Questa struttura dati è utilizzata per capire al volo quando una clausola passa dall'essere soddisfatta all'essere non soddisfatta quando andiamo a porre a True una variabile durante l'esecuzione.
Per ogni variabile \(x_i\) ci segniamo le clausole in cui la variabile appare negata. Questo ci permette di aggiornare il punteggio di tutte le clausole in modo efficiente una volta che settiamo la variabile \(x_i\) a True.
Tutte le clausole con lo score attualmente a \(0\) devono essere mantenuta in una lista.
È possibile trovare una possibile implementazione dell'algoritmo GreedyHorn che fa utilizzo di queste idee nel file horn_satisfiability.py.