Primer 2

Proveriti da li je formula valjana: F=(-p + -q + r) -> -(p*q)

Proveravamo da li je negacija formule nezadovoljiva – ako ne postoji valuacija koja zadovoljava negaciju formule, formula je tačna u svakoj valuaciji, odnosno formula je tautologija.

-F = -(  (-p + -q + r) -> -(p*q)  )

Izvodimo KNF(F):

A->B = -A + B                                   

-(  -(-p + -q + r) + -(p*q)  )

-(A+B) = -A*-B                                 

-(-(-p + -q + r)) * -(-(p*q))

--A=A                                                 

(-p + -q + r) * (p*q)

KNF(F):                                              

(-p + -q + r)*p*q

D={ {-p,-q,r},{p},{q} }

DPLL(D):               Imamo jedinične klauze pa možemo da radimo unit propagation za p i q.

(unit propagation) D[p->1]            (-1 + -q + r)*1*q                D={ {-1,-q,r},{1},{q} }

(zamena negacije literala)            (0 + -q + r)*1*q                 D={ {0,-q,r},{1},{q} }

(brisanje 0 literala)                       (-q + r)*1*q                        D={ {-q,r},{1},{q} }

(tautology)                                    (-q + r)*q                           D={ {-q,r},{q} }

(unit propagation) D[q->1]            (-1 + r)*1                           D={ {-1,r},{1} }

zamena negacije literala              (0 + r)*1                            D={ {0,r},{1} }

(brisanje 0 literala)                       r*1                                     D={ {r},{1} }

(tautology)                                    r                                        D={ {r} }

(unit propagation) D[r->1]             1                                       D={ {1} }

(tautology)                                    ø                                       D={ ø }

(prazan skup)                               return YES

DPLL vraća DA – Negacija formule je zadovoljiva pa formula nije valjana/nije tautologija.