OKPEDIA LOGICA PROPOSIZIONALE

Algoritmo di Davis-Putnam

L'algoritmo di Davis-Putnam ( DP ) è un algoritmo inferenziale applicato alla soddisfacibiltà di un problema di logica proposizionale. L'algoritmo è conosciuto anche con l'acronimo DP. È stato sviluppato negli anni '60 dagli autori Davis e Putnam, diventando fin da subito una pietra miliare degli algoritmi di verifica della soddisfacibilità dei problemi SAT nel logica di 1° grado. L'algoritmo DP è completo, in quanto fornisce una soluzione in un tempo finito, ed è corretto, in quanto la soluzione consente di capire la soddisfacibilità di un problema SAT. Dato un problema espresso nella forma normale congiuntiva ( CNF ) mediante n clausole, l'algoritmo DP applica il metodo della risoluzione su tutti i risolventi per trovare una clausola vuota ( insoddisfacibilità ) oppure una soluzione ( soddisfacibilità ). Durante l'esecuzione l'algoritmo Davis-Putnam utilizza diversi criteri di risoluzione:

  • Clausola unitaria. Le clausole con un solo letterale consentono di effettuare una potatura logica più radicale, in quanto è sufficiente considerare per prima le condizioni di veridicità della clausola unitaria per eliminare gran parte della ramificazione opposta. Il criterio della clausola unitaria è conosciuto anche come "unit rule".
  • Risoluzione ( eliminazione ). Risolvendo le clausole aventi uno stesso letterale opposto, è possibile ottenere una clausola risolvente che sostituisce le clausole originarie. La clausola di eliminazione si basa sul metodo della risoluzione per refutazione. Ad esempio, risolvendo una clausola (A NB) con ( A B) si ottiene una clausola risolvente A che sostituisce le clausole originarie (A NB) con ( A B). Il concetto è conosciuto anche come "elimination rule".
  • Sussunzione. Questo criterio elimina le clausole che possono essere sussunte. Una serie di affermazioni sono sostituite da un gruppo di affermazioni per mezzo di una sostituzione. Il criterio è conosciuto anche come "subsumption rule".
  • Simbolo puro. I letterali puri sono quei letterali che compaiono sempre nella forma negativa o positiva nelle clausole che lo contengono. È possibile sostituire al letterale ( variabile ) il valore booleano che lo verifica ed eliminare le clausole che lo contengono. Il criterio è conosciuto anche come "pure literal rule".

Ad esempio, la seguente formula è espressa in forma normale congiuntiva ( CNF ) ed è composta da tre clausole, ognuna delle quali è una disgiunzione di due letterali:

( A ∨ B ), ( B ∨ C ), ( ¬A ∨ ¬B )

Per verificare la soddisfacibilità della formula è possibile risolvere le clausole per il letterale A, il quale compare in forma positiva nella prima clausola (A) e negativa nella terza clausola (¬A).

( A ∨ B ), ( B ∨ C ), ( ¬A ∨ ¬B )

I letterali complementari A e ¬A si possono eliminare. Dopo la risoluzione ( eliminazione ) per il letterle A la formula può essere riscritta nel seguente modo:

( B ), ( B ∨ C ), ( ¬B )

A questo punto la formula può essere risolta per il letterale B, il quale compare in forma positiva nella prima e nella seconda clausola (B) e in forma negativa nella terza clausola (¬B).

( B ), ( B ∨ C ), ( ¬B )

Risolvendo per il letterale B è possibile eliminare i letterali complementari. Dopo la risoluzione per il letterale B la formula può essere riscritta nel seguente modo:

( C )

Il risultato finale è una clausola unitaria C, quindi il problema è soddisfacibile. Il problema ha una soluzione. Se, durante il processo di risoluzione o nel risultato finale fosse emersa una clausola vuota, allora il problema sarebbe stato insoddisfacibile.

Verifica della soluzione. La verifica della soddisfacibilità del problema e il calcolo della soluzione possono effettuati mediante un processo di assegnazione dei valori booleani alle variabili del problema. Il processo di verifica è il seguente:

VERIFICA SOLUZIONE ALGORITMO DP

  • Primo passo. Nel primo passo viene selezionato il letterale A. Assegnando il valore true al letterale A, la prima clausola ( A ∨ B ) diventa vera ( true ∨ B ) e, quindi, può essere eliminata. Nella terza clausola ( ¬A ∨ ¬B ) il letterale A è, invece, falso poiché in questa clausola è presente il letterale complementare ¬A. Non essendo rilevante, il valore false nella terza clausola ( false ∨ B ) può essere eliminato.
  • Secondo passo. Nel secondo passo la formula risolta con A=true è la seguente: ( B ∨ C ), ( ¬B ). La formula è composta da una disgiunzione ( B ∨ C ) e da una clausola unitaria ( ¬B ). In questi casi è consigliabile analizzare la clausola unitaria ( ¬B ) in modo tale da trovare quale valore booleano ( true/false ) rende vera la clausola. È facile capire che soltanto l'assegnazione B=false può rendere vera la clausola ( ¬B ), essendo quest'ultima composta dalla negazione del valore B. Assegnando il valore false al letterale B la formula può essere riscritta nel seguente modo: ( false ∨ C ), ( ¬false ) che equivale a ( false ∨ C ), ( true ). A questo punto è possibile eliminare la clausola vera ( true ) e il valore false nella disgiunzione. Dopo aver risolto la formula per il letterale B la formula resta composta soltanto dal letterale ( C ).
  • Terzo passo. Nel terzo passo dell'elaborazione è sufficiente verificare quale valore booleano rende vera l'ultima clausola ( C ). È facile verificare che soltanto l'assegnazione C=true può rendere vera la clausola e, quindi, la formula. In conclusione, la soluzione della formula è l'assegnazione A=true, B=false, C=true.
https://www.okpedia.it/algoritmo_di_davis_putnam



note


  • Esempio di soddisfacibilità. Nel seguente esempio la formula è composta da quattro clausole e da tre letterali. La formula viene prima risolta sul letterale A e poi sul letterale B, dando come risultato finale il letterale ¬C. In conclusione, la formula è soddisfacibile poiché la risoluzione non restituisce una clausola vuota.
    ESEMPIO DI SODDISFACIBILITA SAT
  • Esempio di insoddisfacibilità. Nel seguente esempio la formula è composta da quattro clausole e da quattro letterali. La formula viene dapprima risolta sul letterale A, ottenendo per risoluzione una formula composta da tre clausole. La successiva risoluzione per B restituire una clausola vuota e, pertanto, la formula non è soddisfacibile.
    ESEMPIO DI FORMULA INSODDISFACIBILE
    Indipendentemente dai valori che possono assumere i letterali C e D, è sufficiente verificare la contraddizione del letterale B per poter affermare l'insoddisfacibilità della formula.

Logica proposizionale


Questo sito utilizza cookie tecnici. Sono presenti alcuni cookie di terzi ( Gooogle, Facebook ) per la personalizzazione degli annunci pubblicitari. Cliccando su OK, scorrendo la pagina o proseguendo la navigazione in altra maniera acconsenti all’uso dei cookie.

Per ulteriori informazioni o per revocare il consenso fai riferimento alla Privacy del sito.