DPLL

Da Wikipedia, l'enciclopedia libera.

Il DPLL (Davis-Putnam-Logemann-Loveland) è un algoritmo completo, basato sul backtracking, utilizzato per decidere la soddisfacibilità booleana di formule di logica proposizionale in forma normale congiuntiva (CNF), i.e. per risolvere il problema 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 basata sulla risoluzione sviluppata da Davis e Putnam 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.

Algoritmo[modifica | modifica sorgente]

L'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:

Propagazione unitaria
Se una clausola è unitaria, i.e. contiene solo un singolo letterale non assegnato, questa clausola sarà soddisfatta solo assegnando il necessario valore di verità che rende tale letterale vero. Quindi non è necessaria alcuna scelta, e nella pratica ciò porta spesso ad una cascata di clausole unitarie che ridurrà la dimensione dello spazio di ricerca.
Eliminazione dei letterali puri
Se una variabile proposizionale appare nella formula solamente in una polarità, è detta pura. I letterali puri possono essere sempre assegnati in modo da rendere vere tutte le clausole che li contengono. Dunque tali clausole non interessano più la ricerca e possono essere eliminate. Nonostante questa ottimizzazione sia parte del DPLL originale, molte implementazioni attuali la omettono, poiché l'effetto sull'efficienza di tali implementazioni si rivela non calcolabile o, in base al costo della verifica di purezza, addirittura negativo.

L'insoddisfacibilità di un dato assegnamento parziale è verificato se una clausola diventa vuota, i.e. se tutte le sue variabili sono stati 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 pseudocodice, 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, assign(l,Φ) è una funzione che ritorna una formula che è ottenuta sostituendo ogni occorrenza di l con "true" e ogni occorrenza di not l con "false" nella formula Φ, e semplificando la formula risultante. Tale funzione DPLL ritorna solamente quando l'assegnamento finale soddisfa o meno la formula. In una implementazione reale, l'assegnamento soddisfacente la formula è ritornato dall'algoritmo stesso (in questo caso è stato omesso per semplicità).

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 attuali[modifica | modifica sorgente]

Le ricerche attuali si sono svolte in tre direzioni, con lo scopo di migliorare l'algoritmo: definire le differenti politiche sulla scelta della variabile di branching; definire nuove strutture dati che rendano l'algoritmo più veloce, soprattutto nel passo di propagazione unitaria; definire varianti del backtracking su cui si basa. Quest'ultima branca include il backtracking non cronologico e l'apprendimento clausale. Tali raffinamenti permettono di "apprendere" quali siano state le cause (assegnamenti di variabili) che hanno portato ad un conflitto sulle clausole, per poter evitare di giungere ancora a tale stato conflittuale durante il backtracking.

Voci correlate[modifica | modifica sorgente]

Fonti[modifica | modifica sorgente]