Pomoću DPLL algoritma proveriti da li je formula valjana: F=((p+q)*(-p+q)*(p+-q)) => (p*q)
Proveravamo negaciju formule: -F= -( ((p+q)*(-p+q)*(p+-q)) => (p*q) )
Sređujemo formulu u KNF:
A->B = -A + B
-( ((p+q)*(-p+q)*(p+-q)) -> (p*q) ) postaje -( -((p+q)*(-p+q)*(p+-q)) + (p*q) )
-(A+B) = -A * -B
-( -((p+q)*(-p+q)*(p+-q)) + (p*q) ) postaje -(-((p+q)*(-p+q)*(p+-q))) * -(p*q)
-(-A) = A
-(-((p+q)*(-p+q)*(p+-q))) * -(p*q) postaje ((p+q)*(-p+q)*(p+-q)) * -(p*q)
-(A*B) = -A + -B
((p+q)*(-p+q)*(p+-q)) * -(p*q) postaje ((p+q)*(-p+q)*(p+-q)) * (-p + -q)
Uklanjamo suvišne zagrade (asocijativnost):
(p+q)*(-p+q)*(p+-q)*(-p + -q)
Doveli smo izraz u KNF. Možemo da predstavimo i kao
D={ {p,q},{-p,q},{p,-q},{-p,-q} }
Radimo DPLL(D). Jedina operacija koju inicijalno možemo da uradimo je (split)
(split): D[p->1]
(1+q)*(-1+q)*(1+-q)*(-1 + -q) D={ {1,q},{-1,q},{1,-q},{-1,-q} }
(zamena negacije literala)
(1+q)*(0+q)*(1+-q)*(0 + -q) D={ {1,q},{0,q},{1,-q},{0,-q} }
(brisanje 0 literala)
(1+q)*(q)*(1+-q)*( -q) D={ {1,q},{q},{1,-q},{-q} }
(tautology) ako klauza sadrži 1 ili sadrži i p i –p onda može da se ukloni
(q)*(-q) D={ {q},{-q} }
(unit propagation): D[q->1]
(1)*(-1) D={ {1},{-1} }
(zamena negacije literala)
(1)*(0) D={ {1},{0} }
(brisanje 0 literala)
(1)*() D={ {1},{ø} }
(sadrži praznu klauzu)
return NE
vraćamo se na (split) i pokušavamo drugu mogućnost, p=0, pa šta bude
(split): D[p->0]
(0+q)*(-0+q)*(0+-q)*(-0 + -q) D={ {0,q},{-0,q},{0,-q},{-0,-q} }
(zamena negacije literala)
(0+q)*(1+q)*(0+-q)*(1 + -q) D={ {0,q},{1,q},{0,-q},{1,-q} }
(brisanje 0 literala)
(q)*(1+q)*(-q)*(1 + -q) D={ {q},{1,q},{-q},{1,-q} }
(tautology)
(q)*(-q) D={ {q},{-q} }
(unit propagation): D[q->1]
(1)*(-1) D={ {1},{-1} }
(zamena negacije literala)
(1)*(0) D={ {1},{0} }
(brisanje 0 literala)
(1)*() D={ {1},{ø} }
(sadrži praznu klauzu)
return NE i to je konačni rezultat.
Algoritam vraća NE, negacija formule je nezadovoljiva, dakle polazna formula je zadovoljiva/valjana.
Potvrda: uradićemo i tablicu iskaza ((p+q)*(-p+q)*(p+-q)) -> (p*q) = A->B
|
p |
q |
-p |
-q |
p+q |
-p+q |
p+-q |
A |
p*q |
A->B |
|
1 |
1 |
0 |
0 |
1 |
1 |
1 |
1 |
1 |
1 |
|
1 |
0 |
0 |
1 |
1 |
0 |
1 |
0 |
0 |
1 |
|
0 |
1 |
1 |
0 |
1 |
1 |
0 |
0 |
0 |
1 |
|
0 |
0 |
1 |
1 |
0 |
1 |
1 |
0 |
0 |
1 |
Ovo je tautologija, sve interpretacije su zadovoljive.