DPLL
| DPLL | |
|---|---|
 | |
| Clasă | Satisfacție booleană |
| Structură de date | Formule ale logicii propoziționale |
| Cel mai rău caz din punct de vedere temporal | |
| Cel mai rău caz spațial | |
| Costum de afaceri | da |
DPLL ( Davis-Putnam-Logemann-Loveland ) este un algoritm exhaustiv de căutare, bazat pe backtracking , utilizat pentru a decide satisfacția booleană a formulelor logice propoziționale în formă normală conjunctivă (CNF).
A fost introdus în 1962 de Martin Davis , Hilary Putnam , George Logemann și Donald W. Loveland și reprezintă o specializare a algoritmului Davis-Putnam anterior , o procedură dezvoltată în 1960 . Din acest motiv, în special în publicațiile mai vechi, algoritmul Davis-Logemann-Loveland este adesea denumit „metoda Davis-Putnam” sau „algoritmul DP”. Alte nomenclaturi comune care mențin distincția între cele două sunt DLL și DPLL.
DPLL este o procedură foarte eficientă și, după mai bine de 40 de ani, încă stă la baza celor mai eficienți rezolvatori SAT completi, precum și pentru mulți demonstratori de teoreme pentru fragmente de logică de prim ordin .
Algoritm
Algoritmul de backtracking de bază se realizează alegând un literal, atribuindu-i o valoare de adevăr (adevărată sau falsă), simplificând formula și apoi, recursiv, verificând dacă formula simplificată este satisfăcătoare; dacă acesta este cazul, și formula originală este satisfăcătoare; în caz contrar, aceeași procedură recursivă se efectuează presupunând cealaltă valoare de adevăr (falsă sau adevărată). Această procedură este cunoscută sub numele de regulă de împărțire , deoarece împarte problema în două subprobleme mai simple. Pasul de simplificare elimină în esență toate clauzele care au devenit adevărate în acea atribuire de formulă parțială și elimină din clauzele rămase toate literele care au devenit false.
Algoritmul DPLL îmbunătățește backtrack-ul cu utilizarea forțată a acestor reguli, la fiecare pas:
- Propagarea unitară
- Dacă o clauză este unitară , adică conține doar un singur literal neatribuit, această clauză va fi îndeplinită numai prin atribuirea valorii de adevăr necesare care face ca literalul să fie adevărat. Deci nu este necesară nicio alegere și, în practică, acest lucru duce adesea la o cascadă de clauze unitare care vor reduce dimensiunea spațiului de căutare.
- Eliminarea literelor pure
- Dacă o variabilă propozițională apare în formulă numai într-o singură polaritate, se spune că este pură . Literalele pure pot fi întotdeauna atribuite pentru a face adevărate toate clauzele care le conțin. Prin urmare, aceste clauze nu mai afectează cercetarea și pot fi eliminate. Deși această optimizare face parte din DPLL original, multe implementări actuale o omit, deoarece efectul asupra eficienței acestor implementări fie nu este calculabil, fie, pe baza costului verificării purității, este chiar negativ.
Nesatisfăcătorul unei atribuții parțiale date este verificat dacă o clauză devine goală, adică dacă toate variabilele sale au fost atribuite în așa fel încât să facă literele corespunzătoare false. Satisfacția formulei este verificată atunci când toate variabilele sunt atribuite fără a genera clauze goale sau, în implementările moderne, dacă toate clauzele sunt îndeplinite. Nesatisfăcăbilitatea formulei complete poate fi verificată numai după o cercetare exhaustivă a problemei.
Algoritmul DPLL poate fi sintetizat din acest pseudo-cod , unde Φ este formula CNF și μ este o atribuire parțială, inițial goală:
Funcția DPLL (Φ, μ)
dacă Φ = T
apoi reveniți adevărat;
dacă Φ = F
apoi returnează fals;
dacă clauza unitară (l) se găsește în Φ
apoi returnează DPLL (atribuie (l, Φ), μ Λ l);
dacă literalul l se găsește pur în Φ
apoi returnează DPLL (atribuie (l, Φ), μ Λ l);
l: = alege-literal (Φ);
return DPLL (assign (l, Φ), μ Λ l) SAU DPLL (assign (NOT (l), Φ), μ Λ NOT (l));
În acest pseudocod, assign(l,Φ) este o funcție care returnează o formulă care se obține prin înlocuirea fiecărei apariții a lui l cu „adevărat” și a fiecărei apariții a lui not l cu „fals” în formula Φ și simplificarea formulei rezultate . Această funcție DPLL revine numai atunci când atribuirea finală satisface sau nu formula. Într-o implementare reală, atribuirea satisfăcătoare a formulei este returnată de algoritmul însuși (în acest caz a fost omis pentru simplitate).
Algoritmul Davis-Logemann-Loveland are performanțe care depind de alegerea variabilei de ramificare , adică literalul utilizat în etapa de backtracking. După cum puteți vedea, nu avem de-a face cu un algoritm, ci mai bine cu o familie de algoritmi, unul pentru fiecare posibilă alegere cu privire la variabila de ramificare. Eficiența este puternic influențată de această alegere, ducând uneori la diferite instanțe ale problemei care au un timp de execuție constant mai degrabă decât exponențial.
Studii curente
Cercetările pentru îmbunătățirea algoritmului au luat trei direcții:
- definirea diferitelor politici privind alegerea variabilei de ramificare;
- definirea noilor structuri de date pentru a face algoritmul mai rapid, în special în etapa de propagare a unității;
- definirea variantelor algoritmului de backtracking de bază, inclusiv backtracking non-cronologic (backjumping) și învățarea prin clauze . Aceste îmbunătățiri fac posibilă „învățarea” care au fost cauzele (atribuirea variabilelor) care au condus la un conflict asupra clauzelor, pentru a evita atingerea din nou a acestei stări conflictuale în timpul retragerii.
Bibliografie
- (EN) Martin Davis , Putnam, Hillary , A Computing Procedures for Quantification Theory , în Jurnalul ACM , vol. 7, nr. 1, 1960, pp. 201-215.
- (EN) Martin Davis, Logemann, George și Loveland, Donald, Un program pentru teorema mașinilor care demonstrează în comunicațiile ACM , vol. 5, nr. 7, 1962, pp. 394-397.
- ( EN ) Ming Ouyang, cât de bune sunt regulile de ramificare în DPLL? , în Matematică aplicată discretă , vol. 89, nr. 1-3, 1998, pp. 281-286, DOI : 10.1016 / S0166-218X (98) 00045-6 .
Elemente conexe
Alte proiecte
-
Wikimedia Commons conține imagini sau alte fișiere despre DPLL
