Il teorema di Cook-Levin e i SAT-solver

In questa tesi è trattato il tema della soddisfacibilità booleana o proposizionale, detta anche SAT, ovvero il problema di determinare se una formula booleana è soddisfacibile o meno. Soddisfacibile significa che è possibile assegnare le variabili in modo che la formula assuma il valore di verità vero; viceversa si dice insoddisfacibile se tale assegnamento non esiste e se quindi la formula esprime una funzione identicamente falsa. A tal fine si introducono degli strumenti preliminari che permetteranno di affrontare più approfonditamente la questione, partendo dalla definizione basilare di macchina di Turing, affrontando poi le classi di complessità e la riduzione, la nozione di NP-completezza e si dimostra poi che SAT è un problema NP-completo. Infine è fornita una definizione generale di SAT-solver e si discutono due dei principali algoritmi utilizzati a tale scopo.