ZADATAK: Sinhroni brojac sa slike (videti kolokvijum 2015). Izraziti sledece stanje
brojaca u funkciji prethodnog, a zatim dokazati da ako je pocetno stanje jedno
od sledecih: (0,0,0), (1, 0, 1), (1, 0, 0), (0, 1, 1), da se nakon 4 uzastopna 
prelaska brojac vraca u pocetno stanje. 

RESENJE:

Veze izmedju stanja (i = 0,1,2,3): (neka je ovo formula P1)

Ai+1 <=> (Ai /\ Ci) \/ (~Ai /\ ~Ci)
Bi+1 <=> (Ai /\ ~Ci /\ ~Bi)
Ci+1 <=> ~Ci


Pocetni uslovi: (formula P2)
(~A0 /\ ~B0 /\ ~C0) \/ (A0 /\ ~B0 /\ C0) \/ (A0 /\ ~B0 /\ ~C0) \/ (~A0 /\ B0 /\ C0)

Na kraju treba da vazi: (formula Q)

(A0 <=> A4) /\ (B1 <=> B4) /\ (C1 <=> C4)

Treba dokazati: (P1 /\ P2) => Q.

Negacija ove formule P1 /\ P2 /\ ~Q treba da bude nezadovoljiva.

Svodjenje na CNF:

Za veze (i = 0,1,2,3) (ukupno 40 klauza)

~Ai+1 \/ Ai \/ ~Ci
~Ai+1 \/ Ci \/ ~Ai
~Ai \/ ~Ci \/ Ai+1
 Ai \/ Ci \/ Ai+1

~Bi+1 /\ Ai
~Bi+1 /\ ~Ci
~Bi+1 /\ ~Bi
~Ai / Ci \/ Bi \/ Bi+1

~Ci+1 \/ ~Ci
Ci \/ Ci+1

Za pocetne uslove uvodimo nove promenljive s1,s2,s3,s4 (ukupno 17 klauza)

s1 \/ s2 \/ s3 \/ s4

Za s1 <=> ~A0 /\ ~B0 /\ ~C0 imamo:

~s1 \/ ~A0
~s1 \/ ~B0
~s1 \/ ~C0
A0 \/ B0 \/ C0 \/ s1

slicno,

~s2 \/ A0
~s2 \/ ~B0
~s2 \/ C0
~A0 \/ B0 \/ ~C0 \/ s2

~s3 \/ A0
~s3 \/ ~B0
~s3 \/ ~C0
~A0 \/ B0 \/ C0 \/ s3

~s4 \/ ~A0
~s4 \/ B0
~44 \/ C0
A0 \/ ~B0 \/ ~C0 \/ s4

Za ~Q imamo: (ukupno 13 klauza)

~(A0 <=> A4) \/ ~(B1 <=> B4) \/ ~(C1 <=> C4)

uvodimo promenljive T1, T2, T3 kao smene za gornje
ekvivalencije:

~T1 \/ ~T2 \/ ~T3

Za T1 <=> (A0 <=> A4) imamo

~T1 \/ ~A0 \/ A4
~T1 \/ A0 \/ ~A4
T1 \/ ~A0 \/ ~A4
T1 \/ A0 \/ A4

slicno:

~T2 \/ ~B0 \/ B4
~T2 \/ B0 \/ ~B4
T2 \/ ~B0 \/ ~B4
T2 \/ B0 \/ B4

~T3 \/ ~C0 \/ C4
~T3 \/ C0 \/ ~C4
T3 \/ ~C0 \/ ~C4
T3 \/ C0 \/ C4

Sve ukupno ima 70 klauza.

