Davis-Putnam-Logemann-Loveland algoritam definisan je 1961. godine. Služi za dokazivanje zadovoljivosti logičkog iskaza zapisanog u konjuktivnoj normalnoj formi/KNF.
Definicije koje grade DPLL algoritam:
Literal je atomska formula ili njena negacija. U KNF smo literale označavali slovima p,q,r,s... Literal može biti npr. p, q, -p, -q …
Klauza je disjunkcija literala (nekoliko literala povezanih operacijom OR). Klauza bi bila npr.
(-p + q + -r)
Prazna klauza ∅ ne sadrži nijedan literal.
Poredak klauza i literala nije bitan. p+q+r ili q+r+p ima istu vrednost. Formula u KNF može da se posmatra kao skup klauza, jer njihov poredak nije bitan. Isto tako klauza može da se posmatra kao skup literala, jer njihov poredak nije bitan.
Klauza je skup literala, koji se kombinuju operacijom dijunkcije (OR). Formula je skup klauza koje se kombinuju operacijom konjukcije (AND).
Prazna klauza, koja ne sadrži nijedan literal, je nezadovoljiva – ne postoji takav raspored vrednosti literala (zvali smo ih i parametri) koja će dati rezultat Tačno, jer parametara uopšte ni nema. Ovo je granični slučaj, prazan skup.
Formula koja sadrži praznu klauzu je nezadovoljiva.
Prazna formula, koja ne sadrži nijednu klauzu, je zadovoljiva. (interesantna tema za razmišljanje)
Primer predstavljanja formule u DPLL
D – skup klauza. f – formula u KNF. Klauza – skup literala (parametara u klauzi)
Ako je f = (p + q) * (p + -q) onda je D = { {p,q}, {p, -q} }
DPLL algoritam posmatra KNF kao skup klauza koje su skupovi literala, tako da bi trebalo da radimo sa takvom predstavom – algoritam bi u implementaciji koristio tip podataka SET, implementiran u nekom obliku. Pisaćemo formulu uporedo u iskaznom obliku i u obliku skupa klauza.
Prvi korak dokazivanja je da se logička formula F svede u KNF(F). Zatim KNF(F) predstavljamo kao skup klauza D. Nakon toga možemo da izvršimo DPLL(D).
DPLL algoritam
Algoritam je rekurzivan, poziva se nad skupom klauza D dok ne dobijemo rešenje.
Ulaz: D – skup klauza
Izlaz: Da/Ne (D je zadovoljiv/D nije zadovoljiv)
Algoritam (mogući case-ovi u jednom rekurzivnom pozivu):
- (prazan skup)
Ako je D prazan skup (nema klauza) vrati DA - (zamena negacije literala)
Zameni sve literale -0 sa 1 i zameni se literale -1 sa 0- (p + -1) * (-0) à (p + 0) * 1
- (brisanje literala 0)
Obriši sve literale jednake 0- (p + 0) * (q + r + 0) * 0 àp * (q+r) * ∅
- (sadrži praznu klauzu)
Ako D sadrži praznu klauzu vrati NE - (tautology)
Ako neka klauza Ci sadrži T, ili sadrži i literal i negaciju tog literala, ukloni tu klauzu iz D
formalno rečeno, vrati vrednost koju vraća DPLL(D\Ci). Prostim rečima – ukloni klauzu koja je takva da je tautologija, da je garantovano TRUE (tako što ima p OR –p, ili ima TRUE u sebi)- (p+q) * (-p+q+T) * (p+q+-p) * (r+-q) à (p+q)*(r+-q)
- (unit propagation)
Ako je neka klauza jedinična i jednaka nekom iskaznom slovu (ako klauza sadrži samo jedan literal) onda vrati vrednost koju vraća DPLL(D[p->1]), a ako je jednaka –p, vrati DPLL(D[p->0]).
Odnosno – ako se pojavi trivijalna klauza, u kojoj je samo jedan literal, pošto klauza mora da bude tačna onda i taj literal mora da bude tačan, pa smo došli do vrednosti tog literala, i možemo da računamo DPLL gde je ta vrednost poznata od poč
Ako se desi da u jednom koraku dobijemo više takvih klauza, izbor klauze ne utiče na tačnost, ali utiče na efikanost algoritma (jedna od njih će svakako dovesti do razrešenja u manje koraka). Nije nam preterano bitno za sad. - (pure literal)
Ako D sadrži literal p a ne sadrži –p onda vrati vrednost koju vraća DPLL(D[p->1])
a ako sadrži –p a ne sadrži p onda vrati vrednost koju vraća DPLL(D[-p->1])
Odnosno – ako se svuda pojavljuje samo p, onda smo sigurni da je p=1 pa ćemo da zamenimo p sa 1 u celom iskazu, i obrnuto, zamenićemo –p sa 1.
Može se desiti da u jednom koraku imamo više izbora, to ne utiče na tač - (split)
Ako DPLL([p->1]) vraća DA onda vrati DA
inače vrati vrednost koju vraća DPLL([p->0])
Može se desiti da u jednom koraku imamo više izbora, to ne utiče na tačnost.
Isto to zapisano kroz pseudo-kod:
DPLL(D):
(prazan skup)
if D=={}: return YES
(zamena negacije literala)
foreach literal l in D
if l==-1: l=0
if l==-0: l=1
(brisanje 0 literala)
foreach klauza k in D
foreach literal l in k
if l==0:
k.remove(l)
(sadrži praznu klauzu)
foreach klauza k in D
if k=={}: return NO
(tautology)
foreach klauza k in D
foreach literal l in k
if l==1: D.remove(k)
if k.contains(-l): D.remove(k)
(unit propagation)
foreach klauza k in D
if k.literals.count==1:
if k.literals[0] == p //p,q,r...kojigod
D.setValue(p,1)
return DPLL(D)
else //k.literals[0] == not p
D.setValue(p,0)
return DPLL(D)
(pure literal)
foreach literal l in D
if l==p
if D.literals.count(not p) == 0:
D.setValue(p, 1)
return DPLL(D)
if l==not p
if D.literals.count(p) == 0:
D.setValue(p, 0)
return DPLL(D)
(split)
D.setValue(p, 1) //p,q,r…koji god, idi redom
if DPLL(D) == YES:
return YES
else:
D.setValue(p,0)
return DPLL(D)
Osobine DPLL algoritma
Za svaku iskaznu formulu, DPLL procedura se zaustavlja i vraća odgovor DA ako i samo ako je polazna formula zadovoljiva.
Algoritam je eksponencijalne složenosti, O(2N), gde je N broj različitih literala (parametara).
Formula je tautologija ako i samo ako njena negacija nije zadovoljiva.
Formula je kontradikcija ako i samo ako formula nije zadovoljiva.
Formula je poreciva ako i samo ako je njena negacija zadovoljiva.
Formula je valjana ako je negacija formule nezadovoljiva, što je u stvari tautologija.