Algoritmo DPLL con sviluppo di diverse euristiche di splitting


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:

  1. Random Distinct: sceglie casualmente tra i letterali distinti presenti nella formula
  2. 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.
  3. 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.
  4. 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:
  1. L'interfaccia utente
  2. L'implementazione e le strutture dati presenti
  3. Un esempio di debug
  4. L'implementazione e le strutture dati utilizzate
  5. Il funzionamento di ogni euristica e l'analisi delle istanze che dovrebbero garantire performance diverse
  6. I test di benchmark su 3 istanze con relative conclusioni


Link