\documentclass[a4paper,10pt,notitlepage,onecolumn,oneside]{article}

\usepackage[latin2]{inputenc}
\usepackage{amsfonts}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage[serbian]{babel}
\usepackage[T1]{fontenc}

%\renewcommand{\abstractname}{Apstrakt}


%[noend]


\theoremstyle{definition} \newtheorem*{problem}{Zadatak}
\theoremstyle{definition} \newtheorem*{solution}{Rešenje}


\begin{document}

\begin{problem}
Predstaviti 4-bitni potpuni sabirač iskaznom formulom. Zatim pomoću SAT rešavača odrediti razliku dva 4-bitna 
broja. 
\end{problem}

\begin{solution}
Neka su brojevi koje sabiramo $x$ i $y$, i neka je njihov zbir $z$. Tada se broj $x$ može predstaviti iskaznim
varijablama $x_0, x_1, x_2, x_3$ koje odgovaraju binarnim ciframa (počev od cifre najmanje težine). Slično,
broj $y$ se predstavlja iskaznim varijablama  $y_0, y_1, y_2, y_3$, a $z$ varijablama $z_0, z_1, z_2, z_3$.
Prvi zadatak je izraziti varijable $z_i$ preko varijabli $x_i$ i $y_i$:

$$
\begin{array}{l}
 z_0 \Leftrightarrow (x_0 \wedge \neg y_0) \vee (\neg x_0 \wedge y_0) \\
 p_0 \Leftrightarrow (x_0 \wedge y_0) \\
 z_1 \Leftrightarrow (x_1 \wedge \neg y_1 \wedge \neg p_0) \vee 
                     (\neg x_1 \wedge y_1 \wedge \neg p_0) \vee
                     (\neg x_1 \wedge \neg y_1 \wedge p_0) \vee 
                     (x_1 \wedge y_1 \wedge p_0) \\
p_1 \Leftrightarrow  (x_1 \wedge y_1 \wedge \neg p_0) \vee
                     (x_1 \wedge \neg y_1 \wedge p_0) \vee
                     (\neg x_1 \wedge y_1 \wedge p_0) \vee
                     (x_1 \wedge y_1 \wedge  p_0)     \\
 z_2 \Leftrightarrow (x_2 \wedge \neg y_2 \wedge \neg p_1) \vee 
                     (\neg x_2 \wedge y_2 \wedge \neg p_1) \vee
                     (\neg x_2 \wedge \neg y_2 \wedge p_1) \vee 
                     (x_2 \wedge y_2 \wedge p_1) \\
p_2 \Leftrightarrow  (x_2 \wedge y_2 \wedge \neg p_1) \vee
                     (x_2 \wedge \neg y_2 \wedge p_1) \vee
                     (\neg x_2 \wedge y_2 \wedge p_1) \vee
                     (x_2 \wedge y_2 \wedge  p_1)     \\
 z_3 \Leftrightarrow (x_3 \wedge \neg y_3 \wedge \neg p_2) \vee 
                     (\neg x_3 \wedge y_3 \wedge \neg p_2) \vee
                     (\neg x_3 \wedge \neg y_3 \wedge p_2) \vee 
                     (x_3 \wedge y_3 \wedge p_2) \\
p_3 \Leftrightarrow  (x_3 \wedge y_3 \wedge \neg p_2) \vee
                     (x_3 \wedge \neg y_3 \wedge p_2) \vee
                     (\neg x_3 \wedge y_3 \wedge p_2) \vee
                     (x_3 \wedge y_3 \wedge  p_2)     \\
\end{array}
$$
gde su sa $p_0,p_1,p_2,p_3$ označeni redom prenosi sa pozicija $0,1,2,3$. Tranformacijom gornjih definicija u 
CNF, dobijamo:

$$
\begin{array}{llll}
 (\neg z_0 \vee x_0 \vee y_0) & \wedge & (\neg z_0 \vee \neg x_0 \vee \neg y_0) & \wedge \\
 (z_0 \vee \neg x_0 \vee y_0) & \wedge & (z_0 \vee x_0 \vee \neg y_0) & \wedge \\
 (\neg p_0 \vee x_0) & \wedge & (\neg p_0 \vee y_0) & \wedge \\
 (p_0 \vee \neg x_0 \vee \neg y_0) & \wedge & & \\
 (\neg z_1 \vee x_1 \vee y_1 \vee p_0) & \wedge & (\neg z_1 \vee \neg x_1 \vee \neg y_1 \vee p_0) & \wedge \\
 (\neg z_1 \vee x_1 \vee \neg y_1 \vee \neg p_0) & \wedge & (\neg z_1 \vee \neg x_1 \vee y_1 \vee \neg p_0) & \wedge \\
 (z_1 \vee \neg x_1 \vee y_1 \vee p_0) & \wedge & (z_1 \vee x_1 \vee \neg y_1 \vee p_0) & \wedge \\
 (z_1 \vee x_1 \vee y_1 \vee \neg p_0) & \wedge & (z_1 \vee \neg x_1 \vee \neg y_1 \vee \neg p_0) & \wedge \\
 (\neg p_1 \vee x_1 \vee y_1) & \wedge & (\neg p_1 \vee x_1 \vee p_0) & \wedge \\
 (\neg p_1 \vee y_1 \vee p_0) & \wedge & (p_1 \vee \neg x_1 \vee \neg y_1 \vee  p_0) & \wedge \\
 (p_1 \vee \neg x_1 \vee  y_1 \vee \neg p_0) & \wedge & (p_1 \vee x_1 \vee \neg y_1 \vee \neg p_0) & \wedge \\
 (p_1 \vee \neg x_1 \vee \neg y_1 \vee  \neg p_0) & \wedge & & \\ 
 (\neg z_2 \vee x_2 \vee y_2 \vee p_1) & \wedge & (\neg z_2 \vee \neg x_2 \vee \neg y_2 \vee p_1) & \wedge \\
 (\neg z_2 \vee x_2 \vee \neg y_2 \vee \neg p_1) & \wedge & (\neg z_2 \vee \neg x_2 \vee y_2 \vee \neg p_1) & \wedge \\
 (z_2 \vee \neg x_2 \vee y_2 \vee p_1) & \wedge & (z_2 \vee x_2 \vee \neg y_2 \vee p_1) & \wedge \\
 (z_2 \vee x_2 \vee y_2 \vee \neg p_1) & \wedge & (z_2 \vee \neg x_2 \vee \neg y_2 \vee \neg p_1) & \wedge \\
 (\neg p_2 \vee x_2 \vee y_2) & \wedge & (\neg p_2 \vee x_2 \vee p_1) & \wedge \\
 (\neg p_2 \vee y_2 \vee p_1) & \wedge & (p_2 \vee \neg x_2 \vee \neg y_2 \vee  p_1) & \wedge \\
 (p_2 \vee \neg x_2 \vee  y_2 \vee \neg p_1) & \wedge & (p_2 \vee x_2 \vee \neg y_2 \vee \neg p_1) & \wedge \\
 (p_2 \vee \neg x_2 \vee \neg y_2 \vee  \neg p_1) & \wedge & & \\
 (\neg z_3 \vee x_3 \vee y_3 \vee p_2) & \wedge & (\neg z_3 \vee \neg x_3 \vee \neg y_3 \vee p_2) & \wedge \\
 (\neg z_3 \vee x_3 \vee \neg y_3 \vee \neg p_2) & \wedge & (\neg z_3 \vee \neg x_3 \vee y_3 \vee \neg p_2) & \wedge \\
 (z_3 \vee \neg x_3 \vee y_3 \vee p_2) & \wedge & (z_3 \vee x_3 \vee \neg y_3 \vee p_2) & \wedge \\
 (z_3 \vee x_3 \vee y_3 \vee \neg p_2) & \wedge & (z_3 \vee \neg x_3 \vee \neg y_3 \vee \neg p_2) & \wedge \\
 (\neg p_3 \vee x_3 \vee y_3) & \wedge & (\neg p_3 \vee x_3 \vee p_2) & \wedge \\
 (\neg p_3 \vee y_3 \vee p_2) & \wedge & (p_3 \vee \neg x_3 \vee \neg y_3 \vee  p_2) & \wedge \\
 (p_3 \vee \neg x_3 \vee  y_3 \vee \neg p_2) & \wedge & (p_3 \vee x_3 \vee \neg y_3 \vee \neg p_2) & \wedge \\
 (p_3 \vee \neg x_3 \vee \neg y_3 \vee  \neg p_2) &  &  &\\
\end{array}
$$
Razlika dva četvorobitna cela broja se sada može izračunati na sledeći način: pretpostavimo da su nam date cifre zbira
($z_0, z_1, z_2, z_3$) kao i cifre jednog od sabiraka (npr. $y_0, y_1, y_2, y_3$), tada je potrebno odrediti 
cifre drugog sabirka (tj. razlike $x = z - y$), odnoso cifre $x_0, x_1, x_2, x_3$. Ovo se može lako uraditi tako što na
gornju formulu dodamo još jedinične klauze kojima definišemo vrednosti datih cifara. Npr. ako je $z = 1010$ a $y = 0100$
tada je potrebno dodati konjukciju jediničnih klauza $z_3 \wedge \neg z_2 \wedge z_1 \wedge \neg z_0 \wedge \neg y_3
 \wedge y_2 \wedge \neg y_1 \wedge \neg y_0$, a zatim dobijenu formulu propustiti kroz SAT rešavač. Rezultujući model
biće: $\neg x_0, x_1, x_2, \neg p_3, p_2, \neg p_1, \neg p_0$, što daje rezultat $x = 0110$, kao što je i očekivano.
Činjenica da je vrednost varijable $p_3$ jednaka $0$ znači da nije došlo do prenosa na poslednjoj poziciji, tj. 
nema prekoračenja.
\end{solution}



\end{document}
