3      Procedure di approssimazione

Procedura di semi­decisione

Algoritmo greedy semplice

GSAT

Procedura Gu

Pesi

Random walk

Walksat

Novelty

Simulated annealing

Ricerca tabu

Metodi ibridi

Altri approcci

3.1     Procedura di semi­decisione

Papadimitriou ha proposto una procedura di semidecisione per il 2SAT, che modifica ripetutamente l’assegnamento di verità per una variabile in una clausola non soddisfacibile [102]. Questa soddisfa la clausola ma può fare diventare non soddisfacibili altre clausole. Utilizzando un argomento basato sulla rovina del giocatore d'azzardo, Papadimitriou dimostra che, se il problema è poi soddisfacibile questa procedura troverà un assegnamento soddisfacente in O(N²) cambiamenti, con una probabilità che si avvicina ad 3.

Figura 3.1 : La procedura di semidecisione di Papadimitriou per 2­SAT

Esiste anche una procedura di decisione per i problemi Horn­SAT, che modifica le variabili nelle clausole non soddisfacibili e che impiega al massimo N cambiamenti [103].

Questa procedura ha due fasi. Nella prima fase, comincia con un assegnamento che assegna False ad ogni variabile. Allora soddisfa le clausole Horn che contengono un letterale positivo, modificando il valore assegnato ai letterali positivi. Nella seconda fase, esamina le rimanenti clausole negative per determinare se hanno un assegnamento soddisfacente.

Figura 3.2 : La procedura di decisione di Papadimitriou per Horn­Sat

3.2     Algoritmo greedy semplice

Koutsoupias e Papadimitriou hanno presentato una procedura di approssimazione semplice per la soddisfacibilità, che in seguito hanno chiamato algoritmo greedy (goloso) [85]. In questa procedura, si sceglie a caso un assegnamento di verità. Poi si sceglie una variabile tale che modificando i valori di verità aumenta il numero di clausole soddisfatte. Non sono permesse le mosse laterali. Ripetiamo finché nessun miglioramento è possibile. Se questa è una soluzione, consideriamo successo, altrimenti abbandoniamo. Koutsoupias e Papadimitriou hanno dimostrato che questa procedura troverà un assegnamento soddisfacente almeno per tutti i problemi soddisfacibili con O(N²) clausole.

Anche Gent ha proposto un algoritmo greedy altrettanto semplice e che mostra performance ancora migliori. In quest’algoritmo, si assegna semplicemente una variabile secondo la polarità che ha avuto più spesso. Questo troverà un assegnamento soddisfacente per almeno tutti i problemi soddisfacibili con O(Nlog(N)) clausole [32].

Figura 3.3 :  L’algoritmo greedy di Koutsoupias e Papadimitriou

Figura 3.4 : L’algoritmo greedy di Gent

3.3     GSAT

La procedura GSAT [116] aggiunge riavvii e mosse laterali all'algoritmo greedy di Koutsoupias e Papadimitriou. Nonostante la sua semplicità, GSAT e le sue varianti hanno buone performance con una larga varietà di problemi di soddisfacibilità. GSAT comincia con un assegnamento di valori di verità alle variabili generate random, e sale modificando l’assegnamento della variabile che determina il maggior incremento del numero totale di clausole non soddisfatte.

Figura 3.5 : L’algoritmo di ricerca locale GSAT

Se non esiste nessun assegnamento della variabile che può essere modificato per aumentare il risultato, è modificata una variabile che non cambia il risultato. Senza tali modifiche laterali, le performance di GSAT diminuiscono.

Le procedure di ricerca locale, come il GSAT, necessitano che l'implementazione sia fatta con qualche cura. Per ogni iterazione, è modificata soltanto una variabile, e si calcola il numero di clausole soddisfate dopo che la variabile è stata cambiata. Per N variabili e L clausole, il lavoro richiesto è O(NL). Al raggiungimento del numero massimo d’iterazioni, fissato dalla variabile Max-flips, il GSAT ricomincia con un nuovo assegnamento random.

Sebastiani ha descritto come modificare il GSAT in modo che si possa usare con formule non clausali [46]. Lui ha mostrato come calcolare il numero di clausole che potrebbero essere soddisfatte, se le formule fossero convertite in CNF senza costruire la conversione di CNF stessa. Questo calcolo impiega tempo lineare con la dimensione della formula in ingresso.

3.4     Procedura Gu

Nello stesso momento quando è stato presentato il GSAT, Gu ha proposto varie famiglie di procedure di ricerca locale per il SAT [55]. Queste procedure presentano alcune somiglianze con il GSAT. Comunque, loro hanno una struttura di controllo diversa che li permette di muoversi lateralmente quando sono possibili mosse in salita. Non è stato fatto ancora nessun paragone diretto tra le procedure di Gu e la procedura GSAT con le sue versioni.

Figura 3.6 : La famiglia di procedure SAT 1.0 introdotte da Gu

3.5     Pesi

Una modifica della procedura GSAT, che può essere molto utile su una certa classe di problemi, consiste nei pesi delle clausole, introdotte in [112] e [99]. Per ogni clausola è associato un peso che è variato durante la ricerca per focalizzare l’attenzione sulle clausole più difficili. La funzione risultato è la somma dei pesi delle clausole soddisfatte. Selman e Kautz hanno cambiato originalmente solamente i pesi alla fine di ogni prova. Frank ha mostrato che GSAT e HSAT, possono essere migliorate se i pesi sono cambiati dopo ogni modifica [25].

3.6     Random walk

Il successo della procedura di semidecisione di Papadimitriou per il 2SAT e la sua procedura di decisione per il Horn­SAT, illustra i benefici nel focalizzarsi sulle variabili in clausole non soddisfatte (le chiameremo variabili non soddisfatte).

Una versione del GSAT, chiamata GSAT con random walk [114] focalizza alcuni dei suoi sforzi di ricerca sulle variabili non soddisfatte. Il GSAT con random walk modifica con probabilità  p una variabile in una clausola non soddisfatta, altrimenti sale. Modificare una variabile non soddisfatta può far decrescere il numero delle clausole soddisfatte. Ciononostante, il random walk migliora notevolmente le performance del GSAT. Sembra una strategia migliore modificare una variabile non soddisfatta, invece di modificare una variabile random con probabilità  p. In tutti gli assegnamenti soddisfacenti, almeno una delle variabili in una clausola non soddisfatta deve avere il valore di verità opposto. Perciò, dobbiamo modificare almeno una di loro che portano ad un assegnamento soddisfacente.

Siccome la ricerca del GSAT è governata dalle variabili di questo set di clausole non soddisfatte, modificare una variabile non soddisfatta introduce diversità nella ricerca. In [41], Gent e al. hanno mostrato che, uno dei più grandi benefici nell’aggiungere random walk è la riduzione della sensibilità delle performance al parametro Max­Flips.

3.7     WalkSAT

La procedura WalkSAT presentata in [114] prende l'idea di random walk e la inserisce come componente centrale dell'algoritmo. Essenzialmente, il WalkSAT aggiunge i riavvii ed un’euristica per scegliere tra le variabili non soddisfatte alla procedura di decisione di Papadmitriou per 2SAT.

WalkSAT sceglie a caso una clausola non soddisfatta, e poi da questa sceglie una variabile non soddisfatta per modificarla usando un’euristica greedy oppure una random. La scelta esatta è come segue: se una variabile può essere  modificata per soddisfare la clausola senza spezzare nessun'altra clausola, allora la variabile è modificata, altrimenti con la probabilità  p modifichiamo la variabile che spezza il minor numero di clausole, oppure modifichiamo una variabile a caso. Notiamo che, diversamente dal GSAT, la funzione risultato non considera il numero di clausole soddisfatte, ma solamente il numero di clausole che attualmente sono soddisfatte e diventeranno non soddisfatte.

Figura 3.7 : La procedura di ricerca locale WalkSat

3.8     Novelty

Forse ispirato dalle buone performance del WalkSAT e HSAT, l’algoritmo Novelty [93] combina insieme una focalizzazione sulle clausole non soddisfatte con un meccanismo simile al HSAT per variabili modificate che non sono state modificate recentemente. L'algoritmo Novelty ritorna alla funzione di punteggio del GSAT anche il numero delle clausole soddisfatte. L’algoritmo Novelty sceglie in modo random una clausola non soddisfatta. Poi modifica la variabile che presenta il punteggio più alto e che non è l'ultima variabile per essere modificata nella clausola. Se c’è, poi con probabilità  p, Novelty  modifica la variabile col prossimo punteggio più alto, e con probabilità 1-p, la variabile con il punteggio maggiore. L'algoritmo R-Novelty, introdotto sempre in [93], tiene conto della differenza tra i due risultati maggiori. Questo fa la procedura interamente deterministica per pÎ{0, 0.5, 1}. Per inibire i loop, la variabile non soddisfatta è selezionata in modo random ogni 100 cambiamenti.

3.9     Simulated annealing

Simulated annealing non si dimostra così popolare come i metodi di ricerca locale, per esempio il GSAT. I confronti tra i metodi di ricerca locale come il GSAT ed il  simulated annealing dipingono un quadro piuttosto confuso. Per esempio, Selman e Kautz non sono riusciti trovare uno schedule d’annealing che funzioni meglio del GSAT [113].

D'altra parte, Spears ha presentato dei risultati che suggeriscono che simulated annealing funzioni meglio del GSAT sui problemi 3SAT random difficili [121]. Ad oggi non abbiamo nessuna notizia su qualche confronto tra il simulated annealing ed i metodi di ricerca locale come il WalkSAT ed il Novelty, che tendono a funzionare meglio del GSAT su queste classi di problemi.

3.10   Ricerca tabu

Mazure, Sais e Gregoire hanno mostrato che la ricerca tabu funziona bene sui problemi SAT. Loro hanno proposto il TSAT, un algoritmo di ricerca tabu per il SAT [92]. Questo algoritmo tiene una lista FIFO di lunghezza fissa delle variabili modificate. Sui problemi 3SAT random difficili, hanno trovato che la lunghezza ottimale di questa lista tabu aumenta linearmente con N. Hanno mostrato che con tale lista il TSAT era molto competitiva con il WalkSAT.

3.11  Metodi ibridi

C'è stato qualche interesse sui metodi ibridi che combinano insieme le migliori caratteristiche dei metodi approssimati e quelli completi per il SAT. In metodi di ricerca locale possono attraversare rapidamente lo spazio di ricerca. D'altra parte, i metodi completi tendono a seguire traiettorie molto più limitate. Per questo, loro sono compensati da regole propagazione di vincoli come l’unit propagation. Perciò, Zhang e Zhang hanno proposto un metodo ibrido per il SAT che combina insieme un metodo di ricerca locale basato su GSAT ed una procedura sistematica basata sulla procedura di Davis-Putnam [133]. Loro riportano alcuni promettenti risultati su certi problemi di esistenza di quasigroup.

3.12  Altri approcci

Per risolvere i problemi SAT sono state utilizzate anche le reti neurali e gli algoritmi genetici. Un'eccezione è presentata in [120] dove Spears propone un algoritmo di rete Hopfield per risolvere i problemi SAT. La rete è basata su alberi di parsing AND/OR del problema SAT. Spears riporta dei risultati favorevoli sui problemi 3SAT random difficili confrontati con il GSAT. Spears e de Jong  hanno proposto anche un semplice algoritmo genetico per risolvere i problemi SAT [72].

Comunque, sono stati riportati dei risultati insufficienti per determinare se quest’approccio è competitivo con i metodi di ricerca locale come il GSAT.

Hogg e Williams hanno proposto algoritmi quantum per risolvere i problemi SAT. Per esempio, Hogg ha proposto un algoritmo quantum semplice per la soddisfacibilità ed il CSP [60]. Lui ha osservato una phase transition sui problemi 3SAT random come vista nei metodi computazionali classici.

Finalmente, Lipton ha mostrato problemi SAT che utilizzano metodi di calcolo basato su DNA [90].