Algoritmo DPLL - DPLL algorithm

DPLL

In una formula CNF-SAT : 1-Scegli un letterale 2-Assegnagli un valore di verità 3-Semplifica la formula 4-Verifica la soddisfacibilità; 5-Se non sei soddisfatto, fai il backtracking
Classe	Problema di soddisfacibilità booleana
Struttura dati	albero binario
Prestazioni nel caso peggiore	${\displaystyle O(2^{n})}$
Best-caso le prestazioni	${\displaystyle O(1)}$ (costante)
Complessità dello spazio nel caso peggiore	${\displaystyle O(n)}$ (algoritmo di base)

In logica e informatica , il Davis-Putnam-Logemann-Loveland ( DPLL ) algoritmo è un completo , backtracking basata su algoritmo di ricerca per decidere la soddisfacibilità di formule logica proposizionale in forma normale congiuntiva , vale a dire per risolvere il CNF-SAT problema.

È stato introdotto nel 1961 da Martin Davis , George Logemann e Donald W. Loveland ed è un perfezionamento del precedente algoritmo Davis-Putnam , che è una procedura basata sulla risoluzione sviluppata da Davis e Hilary Putnam nel 1960. Soprattutto nelle pubblicazioni più vecchie, il L'algoritmo Davis-Logemann-Loveland viene spesso definito "metodo Davis-Putnam" o "algoritmo DP". Altri nomi comuni che mantengono la distinzione sono DLL e DPLL.

Dopo più di 50 anni, la procedura DPLL costituisce ancora la base per i risolutori SAT completi più efficienti. Recentemente è stato esteso per la dimostrazione automatizzata di teoremi per frammenti di logica del primo ordine mediante l' algoritmo DPLL(T) .

Implementazioni e applicazioni

Il problema SAT è importante sia dal punto di vista teorico che pratico. Nella teoria della complessità è stato il primo problema che si è dimostrato NP-completo e può apparire in un'ampia varietà di applicazioni come il controllo dei modelli , la pianificazione e la programmazione automatizzate e la diagnosi nell'intelligenza artificiale .

In quanto tale, è stato un argomento caldo nella ricerca per molti anni e si svolgono regolarmente competizioni tra i risolutori SAT . Le moderne implementazioni di DPLL come Chaff e zChaff , GRASP o MiniSat sono ai primi posti delle competizioni di questi ultimi anni.

Un'altra applicazione che spesso coinvolge DPLL è la dimostrazione automatizzata di teoremi o le teorie modulo soddisfacibilità (SMT), che è un problema SAT in cui le variabili proposizionali vengono sostituite con formule di un'altra teoria matematica .

L'algoritmo

L'algoritmo di backtracking di base viene eseguito scegliendo un letterale, assegnandogli un valore di verità , semplificando la formula e quindi verificando ricorsivamente se la formula semplificata è soddisfacibile; in tal caso la formula originaria è soddisfacibile; in caso contrario, lo stesso controllo ricorsivo viene eseguito assumendo il valore di verità opposto. Questa è nota come regola di suddivisione , poiché suddivide il problema in due sottoproblemi più semplici. Il passaggio di semplificazione rimuove essenzialmente tutte le clausole che diventano vere sotto l'assegnazione dalla formula e tutti i letterali che diventano false dalle clausole rimanenti.

L'algoritmo DPLL migliora rispetto all'algoritmo di backtracking mediante l'uso ansioso delle seguenti regole in ogni fase:

Propagazione unitaria

Se una clausola è una clausola unit , cioè contiene solo un singolo letterale non assegnato, questa clausola può essere soddisfatta solo assegnando il valore necessario per rendere vero questo letterale. Quindi, nessuna scelta è necessaria. La propagazione unitaria consiste nel rimuovere ogni clausola contenente il letterale di una clausola unitaria e nello scartare il complemento del letterale di una clausola unitaria da ogni clausola contenente quel complemento. In pratica, questo porta spesso a cascate deterministiche di unità, evitando così gran parte dello spazio di ricerca ingenuo.

Pura eliminazione letterale

Se una variabile proposizionale si presenta con una sola polarità nella formula, si dice pure . Un letterale puro può sempre essere assegnato in modo da rendere vere tutte le clausole che lo contengono. Quindi, quando viene assegnato in questo modo, queste clausole non vincolano più la ricerca e possono essere cancellate.

L'insoddisfacibilità di una data assegnazione parziale viene rilevata se una clausola diventa vuota, cioè se tutte le sue variabili sono state assegnate in modo tale da rendere falsi i letterali corrispondenti. La soddisfacibilità della formula viene rilevata o quando tutte le variabili sono assegnate senza generare la clausola vuota, oppure, nelle moderne implementazioni, se tutte le clausole sono soddisfatte. L'insoddisfazione della formula completa può essere rilevata solo dopo un'esauriente ricerca.

L'algoritmo DPLL può essere riassunto nel seguente pseudocodice, dove è la formula CNF :

Algorithm DPLL
    Input: A set of clauses Φ.
    Output: A Truth Value.

function DPLL(Φ)
    if Φ is a consistent set of literals then
        return true;
    if Φ contains an empty clause then
        return false;
    for every unit clause {l} in Φ do
        Φ ← unit-propagate(l, Φ);
    for every literal l that occurs pure in Φ do
        Φ ← pure-literal-assign(l, Φ);
    l ← choose-literal(Φ);
    return DPLL(Φ ∧ {l}) or DPLL(Φ ∧ {not(l)});

In questo pseudocodice, unit-propagate(l, Φ)e pure-literal-assign(l, Φ)sono funzioni che restituiscono il risultato dell'applicazione della propagazione dell'unità e della regola letterale pura, rispettivamente, al letterale le alla formula Φ. In altre parole, sostituiscono ogni occorrenza di lcon "vero" e ogni occorrenza di not lcon "falso" nella formula Φe semplificano la formula risultante. L or' returnnell'istruzione è un operatore di cortocircuito . denota il risultato semplificato della sostituzione di "vero" in . Φ ∧ {l}lΦ

L'algoritmo termina in uno dei due casi. O Φsi scopre che la formula CNF comprende un insieme coerente di letterali , ovvero non c'è le ¬lper nessun letterale lnella formula (ci sono solo letterali puri). Se questo è il caso, le variabili possono essere banalmente soddisfatte impostandole alla rispettiva polarità del letterale comprendente nella valutazione. Altrimenti, quando la formula contiene una clausola vuota, la clausola è vacuamente falsa perché una disgiunzione richiede almeno un membro vero affinché l'insieme complessivo sia vero. In questo caso, l'esistenza di tale clausola implica che la formula (valutata come congiunzione di tutte le clausole) non può essere vera e deve essere insoddisfacente.

La funzione DPLL pseudocodice restituisce solo se l'assegnazione finale soddisfa o meno la formula. In un'implementazione reale, l'assegnazione di soddisfazione parziale in genere viene restituita anche in caso di successo; questo può essere derivato dall'insieme coerente di letterali della prima ifistruzione della funzione.

L'algoritmo di Davis–Logemann–Loveland dipende dalla scelta del letterale di ramificazione , che è il letterale considerato nella fase di backtracking. Di conseguenza, questo non è esattamente un algoritmo, ma piuttosto una famiglia di algoritmi, uno per ogni possibile modo di scegliere il letterale di ramificazione. L'efficienza è fortemente influenzata dalla scelta del letterale di branching: esistono casi in cui il tempo di esecuzione è costante o esponenziale a seconda della scelta dei letterali di branching. Tali funzioni di scelta sono anche chiamate funzioni euristiche o euristiche di ramificazione.

Visualizzazione

Davis, Logemann, Loveland (1961) avevano sviluppato questo algoritmo. Alcune proprietà di questo algoritmo originale sono:

• Si basa sulla ricerca.
• È la base per quasi tutti i moderni risolutori SAT.
• Esso non utilizza l'apprendimento o backtracking non cronologico (introdotto nel 1996).

Un esempio con visualizzazione di un algoritmo DPLL con backtracking cronologico:

• 

  Tutte le clausole che formano una formula CNF

• 

  Scegli una variabile

• 

  Prendi una decisione, variabile a = False (0), quindi le clausole verdi diventano vere

• 

  Dopo aver preso diverse decisioni, troviamo un grafico di implicazione che porta a un conflitto.

• 

  Ora torna indietro al livello immediato e con la forza assegna un valore opposto a quella variabile

• 

  Ma una decisione forzata porta ancora a un altro conflitto

• 

  Torna al livello precedente e prendi una decisione forzata

• 

  Prendi una nuova decisione, ma porta a un conflitto

• 

  Prendi una decisione forzata, ma ancora una volta porta a un conflitto

• 

  Torna al livello precedente

• 

  Continua in questo modo e il grafico di implicazione finale

Lavoro attuale

Negli anni 2010 il lavoro per migliorare l'algoritmo è stato svolto in tre direzioni:

1. Definizione di politiche diverse per la scelta dei letterali di ramificazione.
2. Definizione di nuove strutture dati per rendere più veloce l'algoritmo, in particolare la parte sulla propagazione dell'unità .
3. Definizione di varianti dell'algoritmo di backtracking di base. Quest'ultima direzione include il backtracking non cronologico (noto anche come backjumping ) e l' apprendimento delle clausole . Questi perfezionamenti descrivono un metodo di backtracking dopo aver raggiunto una clausola di conflitto che "apprende" le cause alla radice (assegnazioni alle variabili) del conflitto per evitare di raggiungere nuovamente lo stesso conflitto. I risultanti risolutori SAT di Conflict-Driven Clause Learning sono lo stato dell'arte nel 2014.

Un algoritmo più recente del 1990 è il metodo di Stålmarck . Inoltre dal 1986 (in ordine ridotto) i diagrammi decisionali binari sono stati utilizzati anche per la risoluzione SAT.

Relazione con altre nozioni

Le esecuzioni di algoritmi basati su DPLL su istanze insoddisfacenti corrispondono a prove di confutazione della risoluzione dell'albero .

Guarda anche

• Complessità della prova
• Herbrandizzazione

Riferimenti

Generale

• Davis, Martin ; Putnam, Hilary (1960). "Una procedura di calcolo per la teoria della quantificazione" . Giornale dell'ACM . 7 (3): 201-215. doi : 10.1145/321033.321034 .
• Davis, Martin; Logemann, George; Loveland, Donald (1961). "Un programma macchina per la dimostrazione di teoremi" . Comunicazioni dell'ACM . 5 (7): 394-397. doi : 10.1145/368273.368557 . hdl : 2027/mdp.39015095248095 .
• Ouyang, Ming (1998). "Quanto sono buone le regole di ramificazione in DPLL?" . Matematica Applicata Discreta . 89 (1–3): 281–286. doi : 10.1016/S0166-218X(98)00045-6 .
• John Harrison (2009). Manuale di logica pratica e ragionamento automatizzato . Cambridge University Press. pp. 79-90. ISBN 978-0-521-89957-4.

Specifica

Ulteriori letture

• Malese Ganai; Aarti Gupta; Dott. Aarti Gupta (2007). Soluzioni di verifica formale scalabili basate su SAT . Springer. pp. 23-32. ISBN 978-0-387-69166-4.
• Gomes, Carla P.; Kautz, Henry; Sabharwal, Ashish; Selman, Bart (2008). "Solutori di soddisfacibilità". In Van Harmelen, Frank; Lifschitz, Vladimir; Porter, Bruce (a cura di). Manuale di rappresentazione della conoscenza . Fondamenti dell'intelligenza artificiale. 3 . Altrove. pp. 89-134. doi : 10.1016/S1574-6526(07)03002-7 . ISBN 978-0-444-52211-5.