Algoritmo DPLL con sviluppo di diverse euristiche di splitting
- Studente: Peroni Nicola
- Matricola: VR077942
- Progetto del corso di: Ragionamento Automatico
- Anno Accademico: 2009/2010
- Docente: Alessandro Farinelli
Algoritmo ed euristiche
Algoritmo DPLL con Unit-Propagate. Offre una interfaccia testuale che, oltre all'esecuzione dell'algoritmo
e della scelta dell'euristica, permette all'utente di inserire una formula (fornzandola ad essere CNF),
di caricarca da file (presente nella directory dell'eseguibile) oppure di caricarla da una lista presente
nel file "Formule.dat".
L'implementazione è basata sull'idea di mostrare automaticamente le operazioni che si riprodurrebbero
eseguendo l'algoritmo a penna.
Input: Formula CNF
Output: Soddisfacibilità, tempo di esecuzione, numero di split>
Euristiche di splitting implementate:
- Random Distinct: sceglie casualmente tra i letterali distinti presenti nella formula
- Random Pesato: sceglie casualmente tra i letterali presenti nella formula ripetendoli
(dando quindi "più probabilità" di scelta ad un letterale che si presenta più spesso.
- Letterale Segnato più ricorrente: sceglie il letterale più presente scorrendo tutte le clausole
e tenendo conto del segno (in maniera tale di favorire l'esecuzione di un ramo dell'albero
di ricerca rispetto a quello con il letterale di segno opposto).
L'esecuzione è deterministisca in quanto
parità di ricorrenze viene scelto il primo letterale trovato.
- Letterale più presente nelle clausole più corte: scorre solo le clausole di dimensione più
piccola e sceglie il letterale che si presenta più spesso in tutte queste.
L'esecuzione è deterministisca in quanto
parità di ricorrenze viene scelto il primo letterale trovato
Il codice
Linguaggio utilizzato: c++ con utilizzo direttive dell'ambiente linux.
Il compilatore utilizzato: g++.
Script "Formal_DPLL": e' presente nella root della cartella e ha la funzionalità di lanciare
prima il compilatore del codice (presente in /src) e successivamente l'eseguibile (che si crea in /exe).
Relazione
Nella directory /Relazione è presente il file "Ralazione_Ragionamento.pdf" nella quale vengono presentati
nel dettaglio:
- L'interfaccia utente
- L'implementazione e le strutture dati presenti
- Un esempio di debug
- L'implementazione e le strutture dati utilizzate
- Il funzionamento di ogni euristica e l'analisi delle istanze che dovrebbero garantire performance diverse
- I test di benchmark su 3 istanze con relative conclusioni
Link