10      Conclusioni

Selman e al. hanno comparato vari meccanismi per uscire dai minimi locali in problemi di soddisfacibilità: simulated annealing, random noise, e random walk combinata. La strategia walk introduce perturbazioni nello stato corrente che sono relativi direttamente ai vincoli non soddisfatti del problema. Gli esperimenti di Selman e al. mostrano che questa strategia, migliora significativamente rispetto al simulated annealing e random noise su molte classi di problemi di soddisfacibilità. Le ultime due strategie possono produrre perturbazioni che sembrano meno focalizzate, nel senso che possono coinvolgere variabili che non appaiono in alcuna clausola non soddisfatta.

Il miglioramento relativo trovato utilizzando random walk su altri metodi aumenta con l’aumento della dimensione del problema.

Selman e al. hanno anche mostrato che GSAT con walk è notevolmente efficiente nel risolvere problemi di sintesi dei circuiti. Questo risultato è specialmente interessante perché i problemi di sintesi non hanno nessun elemento casuale, e sono molto difficili per i metodi sistematici.

Finalmente, Selman e al. hanno dimostrato che GSAT con walk migliora anche sui migliori algoritmi per MAX-SAT. Data l'efficacia della strategia random walk combinata su problemi di soddisfacibilità booleana, una direzione interessante per la ricerca futura potrebbe essere l’esplorazione di strategie simili sui problemi con soddisfacimento dei vincoli.

L'incremento del look­back chiaramente rende il DP un algoritmo più efficace. Per quasi ognuna delle istanze esaminate da Bayardo e Schrag, l'apprendimento e CBJ sono stati critici per ottenere delle buone performance. Bayardo e Schrag hanno sospettato che il miglioramento delle performance risultato dall'inclusione del look­back sia infatti dovuto alla sinergia tra le tecniche look-ahead e look­back applicate. L'euristica di selezione della variabile tenta di cercare l'area con i vincoli maggiori dello spazio di ricerca per realizzare al piu presto possibile fallimenti inevitabili. Gli schemi d’apprendimento, attraverso la memorizzazione delle clausole ricavate, possono creare sottospazi di ricerca vincolati da sfruttare dall'euristica di selezione della variabile.

L'apprendimento size-bounded è efficace quando le istanze hanno dei nogood relativamente corti che possono essere ricavati senza inferenza. L'apprendimento relevance-bounded è efficace quando anche molti sottoproblemi che corrispondono all'assegnamento DP corrente hanno questa proprietà. Le scoperte di Bayardo e Schrag indicano che le istanze del mondo reale contengono spesso sottoproblemi con nogoods corti facilmente ricavati. Le istanze della phase transition del 3SAT random tendono ad avere dei nogood molto corti [111], ma questi sembrano richiedere inferenza profonda, ed il DP look-back-enhanced assicura un piccolo vantaggio su di loro [4].

Poche istanze di test sono state non fattibili per il DP look­back-enhanced, ma facili oppure banali per WSAT. Tuttavia, combinando tecniche buone per look-ahead look­back e possibile ottenere performance migliori attraverso una larga serie di problemi.

Li e Ambulagan hanno proposto una procedura di DPL molto semplice che assume solamente delle tecniche look-ahead: un’euristica con ordinamento delle variabili, un controllo di consistenza in avanti FCC e una risoluzione limitata prima della ricerca, dove l'euristica è se stessa basata sull’unit propagation. I risultati sperimentali comparativi del Satz sui problemi 3­SAT random con tre fra le migliori procedure DPL nella letteratura, mostra che questo è molto efficace sui problemi 3­SAT random. Mentre i migliori algoritmi nella letteratura, per risolvere i problemi SAT strutturati, utilizzano di solito le entrambe tecniche, look-ahead e look-back, e accentuano l’ultimo, Satz arriva a migliorare le loro performance su molti problemi SAT strutturati. I risultati suggeriscono che un utilizzo appropriato della tecnica look-ahead, può permettere di fare a meno, per molti problemi SAT strutturati, delle sofisticate tecniche look­-back in una procedura DPL.

Se una procedura DPL è efficace per i problemi SAT random, dovrebbe essere efficace anche per molti problemi strutturati. Per problemi in cui l’euristica UP non riesce a distinguere le variabili, per esempio problemi con molte simmetrie, Satz può essere ancora migliorata con tecniche d’apprendimento.

McAllester e al. hanno presentato due misure statistiche del progresso degli algoritmi di ricerca locale che permettono di trovare rapidamente l’impostazione del noise ottimale. Prima, McAllester e al. hanno mostrato che il valore medio ottimale della funzione obiettivo è approssimativamente costante attraverso le diverse strategie di ricerca locale.

Secondo, McAllester e al. hanno mostrato che si possono ottimizzare le performance di una procedura di ricerca locale misurando il rapporto tra il valore medio e la variazione della funzione obiettivo durante l'esecuzione. La seconda misura permette di trovare buone impostazioni del livello del noise per classi di problema non risolte precedentemente.

Finalmente, McAllester e al. hanno applicato questi principi per valutare le nuove euristiche di ricerca locale, e di conseguenza scoprire due nuove euristiche migliorativi rispetto ad altre versioni del WSAT su tutti i dati di test.

In conclusione possiamo affermare che c'è stato un progresso considerevole fatto nello studio della soddisfacibilità proposizionale negli ultimi 10 anni. Nel presente lavoro ci siamo occupati ad analizzare soltanto alcuni di questi algoritmi, che a nostro parere hanno rappresentato un passo importante nello sviluppo della soddisfacibilità proposizionale. Il progresso è stato sia teoretico che pratico. Sul lato pratico, ora abbiamo procedure di ricerca completi e locali capaci risolvere problemi con centinaio e, in alcuni casi, migliaia di variabili. Molti problemi d’interesse pratico sono stati anche risolti codificandoli in SAT. Sul lato teoretico, abbiamo, un ritratto più sofisticato di quello che rende i problemi SAT difficili da risolvere.Cosa ci può aspettare nel futuro?