• Regolamento Macrocategoria DEV
    Prima di aprire un topic nella Macrocategoria DEV, è bene leggerne il suo regolamento. Sei un'azienda o un hosting/provider? Qui sono anche contenute informazioni per collaborare con Sciax2 ed ottenere l'accredito nella nostra community!

Info WalkSAT

Dvdxseo

Redattore Onorario
Autore del topic
Redattore
User Legend
27 Maggio 2008
5.522
158
Miglior risposta
0
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:
png.latex
Le sotto-formule racchiuse tra le parentesi si chiamano clausole. Assegnando i valori di verità a = true, c = true e dando a b un valore a nostro piacimento vediamo che il risultato di questa formula è true, e quindi la formula è soddisfacibile.
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:
  1. Scegli a caso una clausola ancora non soddisfatta
  2. Lancia una moneta:
    1. Se esce testa cambia il valore di verità assegnato ad una variabile a caso in questa clausola (passo casuale)
    2. 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)
  3. Se la formula adesso è soddisfatta restituisci l'assegnamento corrente.
Ripetendo i passi per un numero massimo max di volte. A questo punto dovrebbe essere chiaro che questo algoritmo potrebbe non darci la soluzione, cioè quando si raggiungono le max iterazioni senza mai aver restituito un assegnamento valido.

In pseudocodice l'algoritmo può essere descritto in questo modo:
Codice:
Perfavore, Entra oppure Registrati per vedere i codici!
Per quanto astratto questo codice ci fa capire bene l'idea alla base di WalkSAT, e cioè quella di combinare un po' di fortuna con un po' di astuzia. La probabilità con cui vengono fatte le scelte casuali (in questo caso 50%) si può ovviamente modificare, si è visto sperimentalmente che di solito il 50% funziona bene o al limite si può dare un pochino più di vantaggio al passo di ottimizzazione, che racchiude in sé l'essenza greedy di questo algoritmo.

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. :emoji_slight_smile: