DPLL

DPLL
	Esempio di backtracking senza backjumping della DPLL
Classe	Soddisfacibilità booleana
Struttura dati	Formule di logica proposizionale
Caso peggiore temporalmente
Caso peggiore spazialmente
Completo	sì

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.

Algoritmo

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, 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, 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

Le ricerche per migliorare l'algoritmo hanno preso tre direzioni:

definizione di differenti politiche sulla scelta della variabile di branching;
definizione di nuove strutture dati per rendere l'algoritmo più veloce, soprattutto nel passo di propagazione unitaria;
definizione di varianti dell'algoritmo base di backtracking, inclusi il backtracking non cronologico (backjumping) e l'apprendimento clausale. Tali raffinamenti permettono di "apprendere" quali sono 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.

Bibliografia

(EN) Martin Davis, Putnam, Hillary, A Computing Procedure for Quantification Theory, in Journal of the ACM, vol. 7, n. 1, 1960, pp. 201-215.
(EN) Martin Davis, Logemann, George, and Loveland, Donald, A Machine Program for Theorem Proving, in Communications of the ACM, vol. 5, n. 7, 1962, pp. 394-397.
(EN) Ming Ouyang, How Good Are Branching Rules in DPLL?, in Discrete Applied Mathematics, vol. 89, n. 1-3, 1998, pp. 281-286, DOI:10.1016/S0166-218X(98)00045-6.

Voci correlate

Altri progetti

Wikimedia Commons contiene immagini o altri file su DPLL

Portale Matematica: accedi alle voci di Wikipedia che trattano di matematica