Implementazione dell'algoritmo DPLL
- Studente: Claudio Meneghello
- Matricola: VR071935
- Insegnamento: Ragionamento automatico
- Anno Accademico: 2009/2010
- Docente: Alessandro Farinelli
Algoritmo ed euristiche
Algoritmo DPLL classico. Data una formula proposizionale nella forma CNF, fornisce un
assegnamento alle variabili che soddisfi la formula o ne indica
l’insoddisfacibilità. La formula viene letta da file. L'utente può
scegliere tra sei euristiche di splitting e se visualizzare l'esecuzione dell'algoritmo
tramite interfaccia testuale.
Input: percorso del file contenente la formula CNF.
Output: Soddisfacibilità, eventuale assegnamento alle variabili,
tempo di esecuzione, numero di split.
Euristiche di splitting implementate:
- Primo letterale della prima clausola: sceglie sempre il primo
letterale trovato.
- Variabile più frequente: sceglie la variabile presente nella
maggior parte delle clausole, indipendentemente dal segno.
- Letterale più frequente: sceglie il letterale presente nella
maggior parte delle clausole tenendo conto del segno.
- Letterale che genera più clausole unitarie: Sceglie il letterale
che permette di ridurre la lunghezza del maggior numero delle clausole
più corte
in modo da generare velocemente clausole unitarie.
- Letterale che elimina clausole corte: sceglie il letterale presente
nella maggior parte delle clausole di dimensione minima.
- Letterale che elimina clausole lunghe: sceglie il letterale presente
nella maggior parte delle clausole di dimensione massima.
L'esecuzione di tutte le euristiche è deterministica in quanto a parità
di occorrenze viene scelto il primo letterale trovato.
Il codice
Linguaggio utilizzato: JAVA.
Compilatore utilizzato: javac.
Esecuzione: Eseguire da terminale il comando
java DPLL <percorso_file_cnf>
Relazione
- Un'introduzione a DPLL.
- Le strutture dati utilizzate.
- L'esecuzione del programma.
- Il comportamento dell'algoritmo principale.
- Le euristiche utilizzate.
- I risultati dei test di benchmark su alcune formule.
Link