|
DPLL
DPLL (Davis-Putnam-Logemann-Loveland) è un algoritmo di ricerca esaustiva, basato sul backtracking, utilizzato per decidere la soddisfacibilità booleana di formule di logica proposizionale in forma normale congiuntiva (CNF), problema noto come CNF-SAT. È stato introdotto nel 1962 da Martin Davis, Hilary Putnam, George Logemann e Donald W. Loveland, e rappresenta una specializzazione del precedente algoritmo di Davis-Putnam, una procedura sviluppata nel 1960. Per questo, soprattutto nelle pubblicazioni più vecchie l'algoritmo Davis-Logemann-Loveland è spesso indicato come il "metodo Davis-Putnam" o "algoritmo DP". Altre nomenclature comuni che mantengono la distinzione fra i due sono DLL e DPLL. Il DPLL è una procedura assai efficiente, e dopo più di 40 anni forma ancora la base dei più efficienti risolutori SAT completi, così come per molti dimostratori di teoremi per frammenti di logica del primo ordine. AlgoritmoL'algoritmo di backtracking di base viene eseguito scegliendo un letterale, assegnandogli un valore di verità (true o false), semplificando la formula e poi, ricorsivamente, verificando se la formula semplificata sia soddisfacibile; se è questo il caso, la formula originale è anch'essa soddisfacibile; altrimenti, si opera la stessa procedura ricorsiva assumendo l'altro valore di verità (false o true). Tale procedimento è noto come splitting rule, poiché divide il problema in due sotto-problemi più semplici. Il passo di semplificazione rimuove, essenzialmente, tutte le clausole che sono diventate vere in quell'assegnamento parziale della formula, ed elimina dalle clausole rimanenti tutti i letterali che sono divenuti falsi. L'algoritmo DPLL potenzia il backtracking con l'utilizzo coatto di queste regole, ad ogni passo:
L'insoddisfacibilità di un dato assegnamento parziale è verificato se una clausola diventa vuota, ovvero se tutte le sue variabili sono state assegnate in modo tale da rendere falsi i letterali corrispondenti. La soddisfacibilità della formula è verificata quando tutte le variabili sono assegnate senza generare alcuna clausola vuota o, nelle implementazioni moderne, se tutte le clausole sono soddisfatte. L'insoddisfacibilità della formula completa può essere verificata solamente dopo una ricerca esaustiva del problema. L'algoritmo DPLL può essere sintetizzato da questo pseudo-codice, dove Φ è la formula CNF e μ è un assegnamento parziale, inizialmente vuoto: funzione DPLL(Φ, μ)
if Φ=T
then return true;
if Φ=F
then return false;
if clausola unitaria (l) si trova in Φ
then return DPLL(assign(l,Φ), μ Λ l);
if letterale l si trova puro in Φ
then return DPLL(assign(l,Φ), μ Λ l);
l := scegli-letterale(Φ);
return DPLL(assign(l,Φ), μ Λ l) OR DPLL(assign(NOT(l),Φ), μ Λ NOT(l));
In questo pseudocodice, L'algoritmo Davis-Logemann-Loveland ha performance che dipendono dalla scelta della variabile di branching, cioè il letterale utilizzato nel passo di backtracking. Come si può notare, non siamo di fronte ad un algoritmo, ma più propriamente ad una famiglia di algoritmi, uno per ogni scelta possibile riguardo alla variabile di branching. L'efficienza è fortemente influenzata da tale scelta, a volte portando a istanze diverse del problema che hanno tempo d'esecuzione costante piuttosto che esponenziale. Studi attualiLe ricerche per migliorare l'algoritmo hanno preso tre direzioni:
Bibliografia
Voci correlateAltri progetti
|
||||||||||||||
Portal di Ensiklopedia Dunia
