Dat je 4-bitni ceo broj x u potpunom komplementu. Dokazati da kada se 
operacija -x u potpunom komplementu uradi dva puta, dobijena vrednost
je jednaka pocetnom broju. Operacija -x se obavlja tako sto se najpre
svi bitovi komplementiraju, a onda se na dobijenu vrednost doda 1.


RESENJE:
--------

Pocetni broj: x3 x2 x1 x0
Nakon prvog potpunog komplementa: y3 y2 y1 y0
Nakon drugog potpunog komplementa: z3 z2 z1 z0

Veza izmedju x i y:

y0 <=> x0
y1 <=> (x0 /\ ~x1) \/ (~x0 /\ x1)
y2 <=> (~x0 /\ ~x1 /\ x2) \/ (x0 /\ ~x2) \/ (x1 /\ ~x2)
y3 <=> (~x0 /\ ~x1 /\ ~x2 /\ x3) \/ (x0 /\ ~x3) \/ (x1 /\ ~x3) \/ (x2 /\ ~x3)

Iz prve ekvivalencije:
[~y0, x0]
[~x0, y0]

Iz druge ekvivalencije:
[~y1, x0, x1]
[~y1, ~x0, ~x1]
[~x0, x1, y1]
[x0, ~x1, y1]

Trecu ekvivalenciju uproscavamo pomocu Cajtinovih smena s1, s2, s3 (za svaku
od konjunkcija sa desne strane ekvivalencije): s1 <=> ~x0 /\ ~x1 /\ x2
s2 <=> x0 /\ ~x2, s3 <=> x1 /\ ~x2. Dobijamo klauze:

[~y2, s1, s2, s3],
[y2, ~s1],
[y2, ~s2],
[y2, ~s3],
[~s1, ~x0],
[~s1, ~x1],
[~s1, x2],
[x0, x1, ~x2, s1],
[~s2, x0],
[~s2, ~x2],
[~x0, x2, s2]
[~s3, x1],
[~s3, ~x2],
[~x1, x2, s3]

Najzad, cetvrtu ekvivalenciju uproscavamo pomocu Cajtinovih smena s4, s5, s6,
s7, kojim zamenjujemo svaku od konjunkcija sa desne strane:

[~y3. s4. s5. s6. s7],
[~s4, y3],
[~s5, y3],
[~s6, y3],
[~s7, y3],
[~s4, ~x0],
[~s4, ~x1],
[~s4, ~x2],
[~s4, x3],
[x0, x1, x2, ~x3, s4],
[~s5, x0],
[~s5, ~x3],
[~x0, x3, s5],
[~s6, x1],
[~s6, ~x3],
[~x1, x3, s6],
[~s7, x2],
[~s7, ~x3],
[~x2, x3, s7]

Slicno se naprave veze izmedju y i z (uvode se pomocne promenljive t1-t7).

Ako sve ove formule zajedno oznacimo sa P, treba dokazati da je P => Q
tautologija, gde je Q:

(x0 <=> z0) /\ (x1 <=> z1) /\ (x2 <=> z2) /\ (x3 <=> z3)

To znaci da treba dokazati da je P /\ ~Q nezadovoljiva formula.

CNF za ~Q:

~(x0 <=> z0) \/ ~(x1 <=> z1) \/ ~(x2 <=> z2) \/ ~(x3 <=> z3)

Uvedimo smene u0 <=> ~(x0 <=> z0), u1 <=> ~(x1 <=> z1),
u2 <=> ~(x2 <=> z2) i u3 <=> ~(x3 <=> z3).

Sada dobijamo klauze:

[u0, u1, u2, u3],
[~u0, x0, z0],
[~u0, ~x0, ~z0],
[~x0, z0, u0],
[x0, ~z0, u0],
[~u1, x1, z1],
[~u1, ~x1, ~z1],
[~x1, z1, u1],
[x1, ~z1, u1],
[~u2, x2, z2],
[~u2, ~x2, ~z2],
[~x2, z2, u2],
[x2, ~z2, u2],
[~u3, x3, z3],
[~u3, ~x3, ~z3],
[~x3, z3, u3],
[x3, ~z3, u3],

Ukupan broj klauza 2 x 39 + 17 = 95.
Broj varijabli: 3x4 + 2x7 + 4 = 30.

