Dejvis–Patnam–Logman–Loveland (DPLL) algoritam

DPLL algoritam je tehnika za rešavanje problema zadovoljivosti bulovih formula, koji pokušava da utvrdi da li postoji kombinacija „tačno“ ili „netačno“ za promenljive koja zadovoljava formulu u konjunktivnoj normalnoj formi (CNF). Ovaj problem je važan u računarstvu, jer je osnova za mnoge logičke i računske probleme.

Istorijat

Ovaj algoritam je razvijen 1961. godine od strane Martina Dejvisa, Džordža Logemana i Donalda V. Lovelanda, kao unapređenje ranijeg Dejvis-Putnam algoritma, koji je razvio Dejvis sa Hilari Putnamom 1960. godine. Algoritam DPLL je često nazivan i "Dejvis-Putnam metodom" ili "DP algoritmom", a u nekim slučajevima se koristi i skraćenica DLL.

Implementacija i primene

SAT problem je veoma važan u računarskim naukama jer se koristi za proveru da li je neka logička formula moguća (zadovoljiva). On je prvi problem koji je dokazano NP-kompletan, što znači da je veoma teško rešiti ga za velike primere.

SAT problem ima mnogo primena, kao što su:

1. Model-čekovanja: Proverava da li neki računarski model radi ispravno.
2. Automatizovano planiranje: Kreiranje planova koji ispunjavaju određene ciljeve.
3. Dijagnoza u veštačkoj inteligenciji: Pronalaženje problema u složenim sistemima.

Za rešavanje SAT problema, koriste se algoritmi kao što je DPLL, koji je veoma popularan u istraživanjima i takmičenjima. U međunarodnim takmičenjima,softveri kao što je Minisat koji koriste DPLL, osvajali su prva mesta.

Algoritam

1. Izbor promenljive i dodela vrednosti: Algoritam bira jednu promenljivu (npr. x) i dodeljuje joj vrednost „tačno“ ili „netačno“. Zatim proverava da li formula postaje tačna ili netačna sa tom dodelom. Ako se formula zadovolji, završavamo – našli smo rešenje. Ako ne, algoritam će kasnije isprobati drugu vrednost (koristeći tzv. backtracking).
2. Jedinične klauze (unit propagation): Ako u formuli postoji klauza sa samo jednim literalom (npr. samo x ili samo ¬x), taj literal mora biti tačan da bi klauza bila ispunjena. Ovim korakom, algoritam uklanja mnogo mogućih dodela vrednosti, jer zna da jedinične klauze moraju biti ispunjene. Primer: ako u formuli postoji samo x, onda algoritam postavlja x na „tačno“.
3. Čiste promenljive : Ako se neka promenljiva pojavljuje samo kao pozitivan (samo x) ili samo kao negativan literal (samo ¬x), može joj se dodeliti vrednost koja zadovoljava sve klauze u kojima se pojavljuje. Na primer, ako imamo x koji se javlja samo u pozitivnom obliku, postavićemo ga na „tačno“, što uklanja sve klauze koje sadrže x, jer su već zadovoljene.
4. Vraćanje unazad (backtracking): Ako nijedna od dodela ne vodi ka rešenju, algoritam se vraća korak unazad (backtrack) i isprobava drugu vrednost za promenljivu. Ovo omogućava algoritmu da isproba sve kombinacije vrednosti ako je potrebno, ali koristeći prednosti jediničnih klauzi i čistih promenljivih da brže eliminiše loše kombinacije.
5. Zaustavljanje: Algoritam se zaustavlja ako:

• Nađe dodelu koja čini formulu tačnom, što znači da je zadovoljiva.
• Ako ne može da zadovolji formulu jer je svaka moguća dodela isprobana i nijedna ne radi, onda zaključuje da formula nije zadovoljiva.

PLL 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, do literala l i formule Φ. Drugim rečima, 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.

Dejvis-Logman-Loveland algoritam zavisi od izbora literala grananja, koji je literal razmotren u bektreking koraku. Kao rezultat toga, ovo nije baš algoritam, već familija algoritama. 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.

DPLL algoritam je veoma važan jer je osnov za većinu modernih SAT softvera, a takođe je povezan i sa mnogim drugim tehnikama u oblasti logike i veštačke inteligencije.