Implementazione della procedura DPLL

attraverso il linguaggio di programmazione JAVA

La procedura DPLL è considerata il metodo computazionalmente più efficiente per valutare se una formula proposizionale S sia soddisfacibile o meno; l'istanza di ingresso della procedura è rappresentata da un insieme di clausole ground (ovvero un insieme dove non appaiono variabili ma solo letterali) in forma normale congiunta (CNF), mentre l'output consiste nel decidere se l'insieme sia soddisfacibile o meno, nel caso in cui lo sia l'algoritmo restituisce un assegnamento che soddisfa l'insieme di clausole.
Quindi, a partire da una formula si cerca di costruire un assegnamento che la verifichi; la procedura può essere vista come un albero di possibili assegnamenti nel quale ciascun nodo rappresenta un insieme di clausole e per ogni nodo ad un letterale viene assegnato un valore di verità; tale valore viene poi propagato per ridurre il numero di assegnamenti futuri.
Un ramo dell'albero non viene più espanso se l'insieme di clausole è vuoto (S è soddisfacibile) oppure se è stata generata la clausola vuota (S è non soddisfacibile). Gli assegnamenti vengono effettuati applicando alcune regole che preservano la soddisfacibilità:

• Tautology Elimination: dall'insieme di clausole vengono eliminate le istanze ground che sono tautologie
• One Literal: se esiste una clausola unitaria LЄS, otteniamo S' da S eliminando quelle clausole ground in S che contengono L. Se S={} allora S è soddisfacibile altrimenti otteniamo un insieme S" da S' eliminando ¬L da tutte le clausole; S è non soddisfacibile se e solo se S" è non soddisfacibile. Quando applichiamo questa regola fissiamo L=Τ nell'assegnamento parziale
• Pure Literal: LЄS è un letterale puro se ¬L non appartiene ad S, se esiste tale letterale allora otteniamo S' rimuovendo tutte le clausole dove appare L (quando questa regola viene applicata, fissiamo L=Τ nell'assegnamento parziale)
• Splitting Rule: se possiamo scrivere S nella forma S = (C₁ ∨ L) ∧ ... ∧ (C_m ∨ L) ∧ (D₁ ∨ ¬L) ∧ ... ∧ (D_m ∨ ¬L) ∧ S_r dove C_i e D_i sono clausole in cui L e ¬L non appaiono e dove S_r è un insieme di clausole dove L e ¬L non appaiono, allora possiamo ottenere due insiemi S'=C₁ ∧ ... ∧ C_m ∧ S_r e S"=D₁ ∧ ... ∧ D_m ∧ S_r. L'insieme S è non soddisfacibile se e solo se S' e S" sono non soddisfacibili. Quando questa regola viene applicata, viene eseguito uno split dell'albero degli assegnamenti e fissiamo L=Τ per il ramo di S" e L=F per il ramo di S'.

Il linguaggio di programmazione scelto per l'implementazione del progetto è JAVA, versione 1.6.0.

• Relazione
• Codice