Algoritmo di Davis-Putnam

L'algoritmo di Davis-Putnam fu sviluppato da Martin Davis e Hilary Putnam allo scopo di verificare la soddisfacibilità booleana (SAT) di formule di logica proposizionale in forma normale congiuntiva (CNF). È un tipo di procedimento di risoluzione nel quale le variabili sono scelte iterativamente ed eliminate, risolvendo ogni clausola in cui questa compaia diretta con ogni clausola in cui compaia negata.

L'algoritmo DP è stato il primo algoritmo per la risoluzione di problemi SAT. Ma questo in generale è molto inefficiente poiché richiede un uso esponenziale della memoria, quindi è adatto a problemi di piccole dimensioni. La sua evoluzione è un algoritmo di ricerca chiamato DPLL. A volte l'algoritmo di Davis–Putnam o DP è scorrettamente usato in riferimento DPLL, ma questi due sono ben distinti.

L'algoritmo funziona nel seguente modo:

 1) elimino tutte le clausole con un solo letterale (unit propagation) |→
        - se la formula contiene le clausole (x) e (¬x) |→ la formula è insoddisfacibile.
        - se la formula contiene la clausola (x) |→
              • elimino tutte le clausole che contengono x.
              • elimino il letterale (¬x) da tutte le altre clausole.
        - se la formula è vuota |→ la formula è soddisfacibile.
 2) per un letterale puro, nella formula compare solamente (x) e non (¬x) |→ assegno x=true
 3) eliminazione di variabili per risoluzione |→
        - per ogni variabile nella formula, ad esempio x |→
              • si producono delle clausole del tipo (A ${\displaystyle \vee }$ B), a partire da coppie (x ${\displaystyle \vee }$ A) e (¬x ${\displaystyle \vee }$ B).
        - una volta risolte ogni coppia di clausole possibili per la variabile x, vengono eliminate tutte le clausole che contengono x e ¬x.

Qui letterale e variabile hanno lo stesso significato.

In generale se ho n clausole che contengono il letterale x e m clausole che contengono il letterale ¬x, eliminerò (n+m) clausole dalla formula, ma per farlo dovrò aggiungere le (n*m) clausole generate. Per questo l'algoritmo ha un notevole consumo di memoria.

Vogliamo verificare se la seguente formula è soddisfacibile.

 (a${\displaystyle \vee }$b) ${\displaystyle \wedge }$ (¬a${\displaystyle \vee }$b) ${\displaystyle \wedge }$ (¬a${\displaystyle \vee }$d) ${\displaystyle \wedge }$ (c) ${\displaystyle \wedge }$ (¬c${\displaystyle \vee }$b${\displaystyle \vee }$¬d) ${\displaystyle \wedge }$ (c${\displaystyle \vee }$d) ${\displaystyle \wedge }$ (a${\displaystyle \vee }$¬d)

1) Eliminiamo le clausole con un solo letterale.

 (a${\displaystyle \vee }$b) ${\displaystyle \wedge }$ (¬a${\displaystyle \vee }$b) ${\displaystyle \wedge }$ (¬a${\displaystyle \vee }$d) ${\displaystyle \wedge }$ (c) ${\displaystyle \wedge }$ (¬c${\displaystyle \vee }$b${\displaystyle \vee }$¬d) ${\displaystyle \wedge }$ (c${\displaystyle \vee }$d) ${\displaystyle \wedge }$ (a${\displaystyle \vee }$¬d) →
 (a${\displaystyle \vee }$b) ${\displaystyle \wedge }$ (¬a${\displaystyle \vee }$b) ${\displaystyle \wedge }$ (¬a${\displaystyle \vee }$d) ${\displaystyle \wedge }$ (b${\displaystyle \vee }$¬d) ${\displaystyle \wedge }$ (a${\displaystyle \vee }$¬d)

2) Assegnamo True ai letterali puri. Abbiamo un solo letterale puro, b. Possiamo quindi eliminare tutte le clausole in cui compare b.

 (a${\displaystyle \vee }$b) ${\displaystyle \wedge }$ (¬a${\displaystyle \vee }$b) ${\displaystyle \wedge }$ (¬a${\displaystyle \vee }$d) ${\displaystyle \wedge }$ (b${\displaystyle \vee }$¬d) ${\displaystyle \wedge }$ (a${\displaystyle \vee }$¬d) →
 (¬a${\displaystyle \vee }$d) ${\displaystyle \wedge }$ (a${\displaystyle \vee }$¬d)

3) Sono rimasti due letterali da risolvere. Scegliamo il letterale a. L'ultima formula può essere riscritta come:

 (¬a${\displaystyle \vee }$d${\displaystyle \vee }$a${\displaystyle \vee }$¬d) →
 (¬a${\displaystyle \vee }$d${\displaystyle \vee }$a${\displaystyle \vee }$¬d) →
 (d${\displaystyle \vee }$¬d) →
 ()

Alla fine otteniamo una formula vuota, quindi la formula originale è soddisfacibile.

• Martin Davis, Putnam, Hilary, A Computing Procedure for Quantification Theory, in Journal of the ACM, vol. 7, n. 1, 1960, pp. 201-215.
• 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.
• R. Dechter and I. Rish. Directional resolution: The Davis-Putnam procedure, revisited. In Proceedings of the Fourth International Conference on the Principles of Knowledge Representation and Reasoning (KR'94), pages 134–145, 1994.

Portale Informatica

Portale Matematica