![cover image](https://wikiwandv2-19431.kxcdn.com/_next/image?url=https://upload.wikimedia.org/wikipedia/commons/thumb/d/dc/Dpll11.png/640px-Dpll11.png&w=640&q=50)
DPLL algoritmus
From Wikipedia, the free encyclopedia
A logikában és az informatikában a Davis–Putnam–Logemann–Loveland (DPLL)-algoritmus egy teljes, visszalépésen (backtrack) alapuló keresőalgoritmus az ítéletlogikai formulák konjunktív normál formában való kielégíthetőségének eldöntésére, azaz a CNF-SAT probléma megoldására.
Gyors adatok
DPLL | |
![]() | |
5 eredménytelen (piros) kísérlet után az a=1, b=1 változó-hozzárendelés kiválasztása, az unitpropagáció után (alul)(zöld) ): a bal felső CNF képlet kielégíthető. | |
Kategória | Boolean satisfiability problem |
Adatstruktúra | Bináris fa |
Legrosszabb időbonyolultság | |
Legjobb időbonyolultság | |
Legrosszabb tár bonyolultság |
Bezárás
Ezt az algoritmust Martin Davis, George Logemann és Donald W. Loveland vezette be 1961-ben, a korábbi Davis-Putnam-algoritmust fejlesztették; a Davis és Hilary Putnam által 1960-ban kifejlesztett rezolúció alapú eljárás volt. Különösen a régebbi publikációkban a Davis–Logemann–Loveland-algoritmust gyakran „Davis–Putnam-módszernek” vagy „DP-algoritmusnak” nevezték. Egyéb gyakori nevek, amik segítik a megkülönböztetést a DLL és a DPLL.