WalkSAT
Il problema SAT (dall'inglese Boolean SATisfiability Problem) è un problema di logica booleana molto famoso in informatica perché è stato il primo problema dimostrato NP-Completo. Questo significa che non conosciamo algoritmi deterministici efficienti sempre corretti per risolvere questo problema.
Il problema si può formulare facilmente avendo delle minime nozioni di logica (come AND e OR) in questo modo: vogliamo trovare un assegnamento di variabili (vero o falso) che rendano vera una formula in Forma Normale Congiuntiva (FNC) che in sostanza è un AND di OR.
Esempio:
Un'osservazione interessante è che qualsiasi formula non in forma normale può essere riscritta in una FNC equivalente.
Non conoscendo algoritmi polinomiali (che, con riferimento alla Tesi di Cook-Karp, possiamo dire "veloci") per risolvere questo problema, i ricercatori si sono ingegnati per trovare dei modi un pochino più furbi del metodo a forza bruta chiaramente improponibile visti gli elevatissimi tempi di esecuzione che richiederebbe per formule poco più complicate. È qui che nasce WalkSAT, un algoritmo greedy per questo problema. Questo algoritmo fa delle scelte casuali nella speranza di arrivare ad una soluzione in questo modo:
- Scegli a caso una clausola ancora non soddisfatta
- Lancia una moneta:
- Se esce testa cambia il valore di verità assegnato ad una variabile a caso in questa clausola (passo casuale)
- Se esce croce cambia il valore di verità di una variabile in modo da massimizzare il numero di clausole soddisfatte dopo questo cambio (passo di ottimizzazione)
- Se la formula adesso è soddisfatta restituisci l'assegnamento corrente.
In pseudocodice l'algoritmo può essere descritto in questo modo:
Codice:
Perfavore,
Entra
oppure
Registrati
per vedere i codici!
Fun fact: ponendo max = ∞ e dando in input una formula non soddisfacibile (cioè tale per cui non esistono assegnamenti che la rendono vera) questo algoritmo non terminerà mai.
Fun fact 2: si è visto che per una buona parte dei problemi 3SAT (cioè SAT con 3 variabili differenti) questo algoritmo necessita, in media, di sole due iterazioni del ciclo for.
Chiaramente questo thread non ha nessuna pretesa di trattare il problema rigorosamente, anzi è volto a stimolare la curiosità verso SAT.