DPLL algoritam

U računarstvu, Dejvis–Patnam–Logman–Loveland (DPLL) algoritam je kompletan, zasnovan na bektreking algoritmom pretrage za odlučivanje zadovoljivosti iskazne logičke formule u konjuktivnoj normalnoj formi, t.j. za rešavanje KNF-SAT problem.

Predstavljen je 1962. godine od strane Martina Dejvisa, Hilari Patnama, Džordža Logmana i Donalda Lovelanda i on je usavršavanje ranijeg Dejvis–Patnam algoritma, koji je rezolucijski-bazirana procedura razvijena od strane Dejvisa i Patnama 1960. godine. Specijalno u starijim publikacijama, Dejvis-Logman-Loveland je često referisan kao “Dejvis-Patnam metod” ili “DP algoritam”. Ostala poznata imena koja održavaju odliku su DLL i DPLL.

Posle skoro 50 godina DPLL procedura i dalje formira osnove za najefikasnije kompletne SAT rešavače. Skoro je proširen za automatizovanu teoremu o dokazivanju za fragmente logike prvog reda.

DPLL

Klasa	Problem zadovoljivosti
Najgora performanca	$O(2^{n})$
Najgora prostorna kompleksnost	$O(n)$ (bazni algoritam)

Implementacije i aplikacije

SAT problem je važan sa obe, teorijske i praktične, tačke gledišta. U kompleksnoj teoriji bio je prvi dokazan problem da je NP-kompletan, i može da se pojavi u širokom spektru aplikacija kao što su provera modela, automatizovano planiranje i raspoređivanje, i dijagnoza u veštačkoj inteligenciji.

Kao takav, bio je i još je popularna tema u istraživanju već dugi niz godina, i takmičenja između SAT rešavača se redovno održavaju. DPLL-ove moderne implementacije kao Chaff i zChaff, GRASP ili Minisat su na prvim mestima u takmičenjima poslednjih godina.

Još jedna aplikacija koja često uključuje DPLL je automatizovana teorema dokazivanja ili zadovoljivosti modulo teorije koje je SAT problem u kojem iskazne promenljive su zamenjene sa formulama drugih matematičkih teorija.

Algoritam

Osnovni bektreking algoritam se pokreće izborom literala, prepisujući mu tačnu vrednost, pojednostavljivanjem formule potom i rekurzivne provere da lu je formula zadovoljiva; ako je ovo slučaj, originalna formula je zadovoljiva; u suprotnom, ista rekurzivna provera se obavlja pod pretpostavkom netačne vrednosti. Ovo je poznato kao splitting rule, jer deli problem na dva jednostavnija potproblema. Korak pojednostavljivanja u suštini briše sve klauze koje su postale tačne po dodeli iz formule, i svi literali koji su postali netačni iz preostalih klauza.

DPLL algoritam se poboljšava preko bektreking algoritma po željenoj upotrebi sledećih pravila u svakom koraku:

Unit propagation

Ako je klauza jedinična klauza, t.j. sadrži samo jedan nedodeljen literal, ova klauza može biti jedino zadovoljiva dodeljivanjem neophodne vrednosti da bi ovaj literal bio tačan. Prema tome, nije potreban izbor. U praksi, ovo često vodi do determinističkih kaskada jedinica, prema tome izbegava veliki deo naivne pretrage prostora.

Pure literal elimination

Ako se iskazna promenljiva javlja samo sa jednim polaritetom u formuli, zove se čista. Čisti literali mogu uvek biti dodeljeni na način koji čine sve klauze koje ih sadrže tačne. Prema tome, te klauze više ne ograničavaju pretragu i mogu biti obrisane.

Nezadovoljivost datog delimičnog zadatka je otkrivena ako jedna klauza postane prazna t.j. ako sve njene promenljive su dodeljene tako što čini odgovarajuće literele netačnim. Zadovoljivost formule se otkriva bilo kada sve promenljive su dodeljene bez stvaranja prazne klauze, ili, u modernim inplementacijama, ako su sve klauze zadovoljene. Nezadovoljivost komletne formule može biti otkrivena jedino nakon iscrpne pretrage.

DPLL algoritam se može rezimirati u sledećem pseudokodu, gde je Φ je KNF formula:

  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 Φ
      Φ ← unit-propagate(l, Φ);
   for every literal l that occurs pure in Φ
      Φ ← pure-literal-assign(l, Φ);
   l ← choose-literal(Φ);
   return DPLL(Φ ∧ l) or DPLL(Φ ∧ not(l));

U ovom pseudokodu, unit-propagate(l, Φ) i pure-literal-assign(l, Φ) su funkcije koje vraćaju rezultat primene pravila unit propagation i the pure literal, respektivno, do literala l i formule Φ. Drugim recima, one zamenjuju svako pojavljivanje l sa "tačno" i svako pojavljivanje not l sa "netačno" u formuli Φ, i pojednostavljuje rezultujuću formulu. or u return iskaz je operator kratkog spoja. Φ ∧ l označava pojednostavljen rezultat zamene "tačno" za l u Φ.

Pseudokod DPLL funkcija vraća samo da li je krajnja dodela zadovoljava formulu ili ne. U realnoj implementaciji, delimična zadovoljiva formula obično takođe vraća uspeh; ovo se može izvesti iz konzistentnog skupa literala prvog if izraza u funkciji.

Dejvis-Logman-Loveland algoritam zavisi od izbora literala grananja, koji je literal razmotren u bektreking koraku. Kao rezultat toga, ovo nije baš algotitam, već familija algoritama, jedan za svaki mogući način izbora literala grananja. Efikasnost je jako pogođena izborom literala grananja: postoje instance za koje je vreme izvršavanja konstantno ili eksponencijalno u zavisnosti od izbora literala grananja. Takve funkcije se takođe zovu heurističke funkcije ili heuristike grananja.

Trenutni rad

u 2010. godini, rad na poboljšanju algoritma je urađen u tri pravca:

1. Definisanje različitih politika za izbor literala grananja
2. Definisanje nove satrukture podataka da bi algoritam postao brži, posebno za deo unit propagation
3. Definisanje varijante bazičnog backtracking algoritma. Drugi pravac obuhvataju ne hronološki Bektreking (ili backjumping) i učenje klauza. Ova poboljšanja opisuju metodu bektreking nakon postizanja konflikt klauze koja "uči" osnovne uzorke (zadatke za promenljive) konflikta kako bi se izbeglo dostizanje istog konflikta ponovo. Dobijeni Conflict-Driven Clause Learning SAT rešavači su stanje umetnosti u 2014. godini.

Odnos sa drugim pojmovima

Rad na DPLL baziranim algoritmima na nezadovoljivim slučajevima odgovaraju stablu rezolucije za pobijanje dokaza.

Reference

General

• Davis, Martin; Putnam, Hilary (1960). „A Computing Procedure for Quantification Theory”. Journal of the ACM. 7 (3): 201—215. S2CID 31888376. doi:10.1145/321033.321034. 
• Davis, Martin; Logemann, George; Loveland, Donald (1962). „A Machine Program for Theorem Proving”. Communications of the ACM. 5 (7): 394—397. S2CID 15866917. doi:10.1145/368273.368557. hdl:2027/mdp.39015095248095. 
• Ouyang, Ming (1998). „How Good Are Branching Rules in DPLL?”. Discrete Applied Mathematics. 89 (1–3): 281—286. doi:10.1016/S0166-218X(98)00045-6. 
• Harrison, John (2009). Handbook of practical logic and automated reasoning. Cambridge University Press. str. 79–90. ISBN 978-0-521-89957-4. 

Specific

Literatura

• Marques-Silva, João (1999). „The Impact of Branching Heuristics in Propositional Satisfiability Algorithms”. Progress in Artificial Intelligence. Lecture Notes in Computer Science. 1695. str. 62—74. ISBN 978-3-540-66548-9. doi:10.1007/3-540-48159-1_5. 
• Beek, Peter Van (2006). „Backtracking search algorithms”. Ur.: Francesca Rossi, Peter Van Beek, Toby Walsh. Handbook of constraint programming. Elsevier. str. 122. ISBN 978-0-444-52726-4. CS1 održavanje: Višestruka imena: spisak urednika (veza)