Abstract

Il presente elaborato, si propone di fare un riassunto dello sviluppo degli algoritmi per la soddisfacibilità proposizionale, con un approfondimento su alcuni degli algoritmi che si sono evidenziati per le notevoli performance.

Nel Capitolo 1 sono definiti i concetti di ricerca sistematica e locale, problemi NP-completi e NP-hard, logica proposizionale e soddisfacibilità, forme normali, problemi con soddisfacimenti di vincoli.

Il Capitolo 2 si concentra sulle procedure complete per SAT ed argomenti come le euristiche, le strutture di dati e la loro realizzazione, backtracking ed apprendimento, risoluzione ed altri approcci.

Il Capitolo 3 evidenzia le principali caratteristiche di alcune procedure non complete come greedy, GSAT, random walk, Walksat, Novelty mentre nel Capitolo5 si fa un riassunto dei principali tipi di problemi affrontati dagli algoritmi SAT.

Cominciando con il Capitolo 6 si entra nello studio approfondito degli algoritmi che rappresentano il tema del presente elaborato.

Seguono le conclusioni nel Capitolo 10, link delle biblioteche di benchmark nel Capitolo 11 e la bibliografia nel Capitolo 12.

Per la realizzazione di questo elaborato sono stati utilizzati vari pubblicazioni tra cui si notano The Search for Satisfaction di Gent e Walsh [44], Noise Strategies for Improving Local Search di Selman, Kautz e Cohen [114], Using CSP look­back techniques to solve exceptionally hard SAT instances di Bayardo  e Schrag [4], Look-ahead versus look-back for satisfiability problems di Li e Ambulagan [89], Evidence for invariants in local search di McAllester, Selman, e Kautz [93] e la tesi di dottorato di H. Hoos Stochastic Local Search ­ Methods, Models, Applications [66].