CNF-SAT: Sat Solver with Backtracking and Graph-Based Backjumping

Introduzione al CNF-SAT

In questo elaborato è stato trattato il problema denominato CNF-SAT ossia quello di decidere la soddisfacibilità booleana di formule di logica proposizionale in forma normale congiuntiva (CNF).

L'algoritmo usato è il DPLL con Backtracking e Backjumping Graph-Based, sono previste come euristiche la FOV (First Order Variable), MRV (Minimum Remaining Values) e la LCV (Least Constrained Variable).

Algoritmi di risoluzione

• Backtracking: può essere descritto come una depht-first su grafo implicito. Un grafo implicito è un grafo non noto a priori, ogni mossa lungo il grafo corrisponde ad aggiungere un nuovo elemento alla soluzione. Se procedendo, si arriva a terminare la soluzione ammissibile, la ricerca ha successo. Se invece si arriva ad un nodo per cui non è possibile completare la soluzione, si torna indietro fino al primo nodo che ha ancora dei vicini non visitati, dai quali la ricerca riprende.
• Graph-Based Backjumping: trattasi di un miglioramento applicato al Backtracking applicando uno schema di tipo Lookback. L'idea di base è che quando non si può più espandere il grafo implicito si effettua un salto indietro non di un passo ma ad una variabile chiamata culprit, che corrisponde alla variabile più vicina fra quelle in conflitto con l'attuale nodo, ovvero fra quelle "colpevoli" del fallimento.

Implementazione

• MYDPLL: Il sorgente principale contentente le implementazioni dei due metodi per il DPLL
• GRAFO: La classe che rappresenta il grafo implicito

Risultati

• Relazione
• Codice