\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}
Četiri čoveka nose prezimena Smith, Baker, Carpenter i Tailor i imaju neku od četiri profesije: kovač (smith), 
pekar (baker), stolar (carpenter) i krojač (tailor), ali ni jedan od njih nema profesiju koja je sadržana u 
njegovom prezimenu. Takođe, svaki od njih ima po jednog sina koji se takođe bave nekom od ove četiri profesije,
ali takođe niko onom profesijom koja je sadržana u njegovom prezimenu. Niko od sinova nema istu profesiju kao
svoj otac. Baker ima istu profesiju kao Carpenter-ov sin, dok je Smith-ov sin pekar. Pronaći profesije očeva
i sinova.  
\end{problem}

\begin{solution}
Uvodimo iskazne varijable $x_{ij}$ koje označavaju da se čovek $i$ bavi profesijom $j$ (pri čemu i osobe i profesije
indeksiramo onim redom kako je navedeno u tekstu zadatka). Uslovi da se svaki od četiri čoveka bavi nekom od četiri
profesije mogu se iskazati na sledeći način:

$$
\begin{array}{ll}
 (x_{11} \vee x_{12} \vee x_{13} \vee x_{14}) & \wedge \\
 (x_{21} \vee x_{22} \vee x_{23} \vee x_{24}) & \wedge \\
 (x_{31} \vee x_{32} \vee x_{33} \vee x_{34}) & \wedge \\
 (x_{41} \vee x_{42} \vee x_{43} \vee x_{44}) & \\
\end{array}
$$
Uslovi da se svaki od njih bavi tačno jednom profesijom , tj. da se ne može istovremeno baviti nekim parom
gornjih profesija iskazuju se na sledeći način:

$$
\begin{array}{ll}
 (\neg x_{11} \vee \neg x_{12}) & \wedge \\
 (\neg x_{11} \vee \neg x_{13}) & \wedge \\
 (\neg x_{11} \vee \neg x_{14}) & \wedge \\
 (\neg x_{12} \vee \neg x_{13}) & \wedge \\
 (\neg x_{12} \vee \neg x_{14}) & \wedge \\
 (\neg x_{13} \vee \neg x_{14}) & \wedge \\
 (\neg x_{21} \vee \neg x_{22}) & \wedge \\
 (\neg x_{21} \vee \neg x_{23}) & \wedge \\
 (\neg x_{21} \vee \neg x_{24}) & \wedge \\
 (\neg x_{22} \vee \neg x_{23}) & \wedge \\
 (\neg x_{22} \vee \neg x_{24}) & \wedge \\
 (\neg x_{23} \vee \neg x_{24}) & \wedge \\
 (\neg x_{31} \vee \neg x_{32}) & \wedge \\
 (\neg x_{31} \vee \neg x_{33}) & \wedge \\
 (\neg x_{31} \vee \neg x_{34}) & \wedge \\
 (\neg x_{32} \vee \neg x_{33}) & \wedge \\
 (\neg x_{32} \vee \neg x_{34}) & \wedge \\
 (\neg x_{33} \vee \neg x_{34}) & \wedge \\
 (\neg x_{41} \vee \neg x_{42}) & \wedge \\
 (\neg x_{41} \vee \neg x_{43}) & \wedge \\
 (\neg x_{41} \vee \neg x_{44}) & \wedge \\
 (\neg x_{42} \vee \neg x_{43}) & \wedge \\
 (\neg x_{42} \vee \neg x_{44}) & \wedge \\
 (\neg x_{43} \vee \neg x_{44}) & \wedge \\
\end{array}
$$
Uslovi da se niko ne bavi profesijom sadržanom u svom prezimenu mogu se predstaviti kao:

$$
\neg x_{11} \wedge \neg x_{22} \wedge \neg x_{33} \wedge \neg x_{44}
$$
Po sličnom principu, uvodimo iskazne varijable $y_{ij}$ koje označavaju da se $i$-ti sin bavi $j$-tom profesijom.
Sasvim slično, uvodimo skup klauza koje definišu uslove da se sinovi bave nekom (tačno jednom) od četiri profesije,
kao i da se ne bave profesijom sadržanom u svom prezimenu:

$$
\begin{array}{ll}
 (y_{11} \vee y_{12} \vee y_{13} \vee y_{14}) & \wedge \\
 (y_{21} \vee y_{22} \vee y_{23} \vee y_{24}) & \wedge \\
 (y_{31} \vee y_{32} \vee y_{33} \vee y_{34}) & \wedge \\
 (y_{41} \vee y_{42} \vee y_{43} \vee y_{44}) & \wedge \\
 (\neg y_{11} \vee \neg y_{12}) & \wedge \\
 (\neg y_{11} \vee \neg y_{13}) & \wedge \\
 (\neg y_{11} \vee \neg y_{14}) & \wedge \\
 (\neg y_{12} \vee \neg y_{13}) & \wedge \\
 (\neg y_{12} \vee \neg y_{14}) & \wedge \\
 (\neg y_{13} \vee \neg y_{14}) & \wedge \\
 (\neg y_{21} \vee \neg y_{22}) & \wedge \\
 (\neg y_{21} \vee \neg y_{23}) & \wedge \\
 (\neg y_{21} \vee \neg y_{24}) & \wedge \\
 (\neg y_{22} \vee \neg y_{23}) & \wedge \\
 (\neg y_{22} \vee \neg y_{24}) & \wedge \\
 (\neg y_{23} \vee \neg y_{24}) & \wedge \\
 (\neg y_{31} \vee \neg y_{32}) & \wedge \\
 (\neg y_{31} \vee \neg y_{33}) & \wedge \\
 (\neg y_{31} \vee \neg y_{34}) & \wedge \\
 (\neg y_{32} \vee \neg y_{33}) & \wedge \\
 (\neg y_{32} \vee \neg y_{34}) & \wedge \\
 (\neg y_{33} \vee \neg y_{34}) & \wedge \\
 (\neg y_{41} \vee \neg y_{42}) & \wedge \\
 (\neg y_{41} \vee \neg y_{43}) & \wedge \\
 (\neg y_{41} \vee \neg y_{44}) & \wedge \\
 (\neg y_{42} \vee \neg y_{43}) & \wedge \\
 (\neg y_{42} \vee \neg y_{44}) & \wedge \\
 (\neg y_{43} \vee \neg y_{44}) & \wedge \\
 \neg y_{11} & \wedge \\
 \neg y_{22} & \wedge \\
 \neg y_{33} & \wedge \\
 \neg y_{44} & \\
\end{array}
$$
Uslovi da se sinovi ne bave istim profesijama kao njihovi očevi mogu se izraziti na sledeći način:

$$
\begin{array}{ll}
(\neg x_{11} \vee \neg y_{11}) & \wedge \\
(\neg x_{12} \vee \neg y_{12}) & \wedge \\
(\neg x_{13} \vee \neg y_{13}) & \wedge \\
(\neg x_{14} \vee \neg y_{14}) & \wedge \\
(\neg x_{21} \vee \neg y_{21}) & \wedge \\
(\neg x_{22} \vee \neg y_{22}) & \wedge \\
(\neg x_{23} \vee \neg y_{23}) & \wedge \\
(\neg x_{24} \vee \neg y_{24}) & \wedge \\
(\neg x_{31} \vee \neg y_{31}) & \wedge \\
(\neg x_{32} \vee \neg y_{32}) & \wedge \\
(\neg x_{33} \vee \neg y_{33}) & \wedge \\
(\neg x_{34} \vee \neg y_{34}) & \wedge \\
(\neg x_{41} \vee \neg y_{41}) & \wedge \\
(\neg x_{42} \vee \neg y_{42}) & \wedge \\
(\neg x_{43} \vee \neg y_{43}) & \wedge \\
(\neg x_{44} \vee \neg y_{44}) & \\
\end{array}
$$
Najzad, uslov da se Baker bavi istom profesijom kao Carpenter-ov sin se izražava kao 
$(x_{21} \wedge y_{31}) \vee (x_{22} \wedge y_{32}) \vee (x_{23} \wedge y_{33}) \vee (x_{24} \wedge y_{34})$, što
se transformacijom u CNF svodi na sledeći skup klauza:

$$
\begin{array}{ll}
(x_{21} \vee x_{22} \vee x_{23} \vee x_{24}) & \wedge \\
(x_{21} \vee x_{22} \vee x_{23} \vee y_{34}) & \wedge \\
(x_{21} \vee x_{22} \vee y_{33} \vee x_{24}) & \wedge \\
(x_{21} \vee x_{22} \vee y_{33} \vee y_{34}) & \wedge \\
(x_{21} \vee y_{32} \vee x_{23} \vee x_{24}) & \wedge \\
(x_{21} \vee y_{32} \vee x_{23} \vee y_{34}) & \wedge \\
(x_{21} \vee y_{32} \vee y_{33} \vee x_{24}) & \wedge \\
(x_{21} \vee y_{32} \vee y_{33} \vee y_{34}) & \wedge \\
(y_{31} \vee x_{22} \vee x_{23} \vee x_{24}) & \wedge \\
(y_{31} \vee x_{22} \vee x_{23} \vee y_{34}) & \wedge \\
(y_{31} \vee x_{22} \vee y_{33} \vee x_{24}) & \wedge \\
(y_{31} \vee x_{22} \vee y_{33} \vee y_{34}) & \wedge \\
(y_{31} \vee y_{32} \vee x_{23} \vee x_{24}) & \wedge \\
(y_{31} \vee y_{32} \vee x_{23} \vee y_{34}) & \wedge \\
(y_{31} \vee y_{32} \vee y_{33} \vee x_{24}) & \wedge \\
(y_{31} \vee y_{32} \vee y_{33} \vee y_{34}) &  \\
\end{array}
$$
I na kraju, uslov da je Smith-ov sin pekar izražava se jediničnom klauzom $y_{12}$.
Ovaj skup klauza treba predati SAT rešavaču. Profesije očeva i sinova biće određene
varijablama kojima je u zadovoljavajućoj valuaciji dodeljena vrednost $1$. 

Naš prototipski DPLL-zasnovan SAT rešavač daje sledeći model (prikazujemo samo varijable kojima je
dodeljena vrednost $1$):

$$
x_{13}, x_{21}, x_{32}, x_{41}, y_{12}, y_{23}, y_{31}, y_{42}
$$
(Smith je stolar, Baker je kovač, Carpenter je pekar, Tailor je kovač, Smith-ov sin je pekar, Baker-ov sin je
stolar, Carpenter-ov sin je kovač, dok je Tailor-ov sin pekar), dok je MINISAT vratio sledeći model:
$$
x_{14}, x_{21}, x_{32}, x_{42}, y_{12}, y_{23}, y_{31}, y_{41}
$$
(Smith je krojač, Baker je kovač, Carpenter je pekar, Tailor je pekar, Smith-ov sin je pekar, Baker-ov sin je
stolar, Carpenter-ov sin je kovač, dok je Tailor-ov sin kovač).
Lako se da proveriti da dati modeli zadovoljavaju sve tražene uslove. Takođe, primećujemo da 
rešenje ovog zadatka nije jedinstveno.

\end{solution}



\end{document}
