\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}
Dat je dvocifreni binarni brojač. Protokom vremena brojač menja svoje
stanje: $00 \rightarrow 01 \rightarrow 10 \rightarrow 11 \rightarrow 00 \rightarrow 01 \rightarrow \ldots{}$
\begin{itemize}
\item[a)] Iskaznom formulom opisati vezu između dva uzastopna stanja: $p_iq_i \rightarrow p_{i+1}q_{i+1}$.
\item[b)] Korišćenjem \emph{minisat}-a dokazati da se nakon 4 prelaza dobija isto
početno stanje.
\end{itemize}
\end{problem}

\begin{solution}
Veze između $p_iq_i$ i $p_{i+1}q_{i+1}$ (za $i = 0, 1, 2, 3$), date su sa:

$$
\begin{array}{l}
q_{i+1} \Leftrightarrow \neg q_i \\
p_{i+1} \Leftrightarrow (\neg q_i \wedge p_i) \vee (q_i \wedge \neg p_i) 
\end{array} 
$$
Svođenjem na CNF, dobija se sledeći skup klauza:

$$
\begin{array}{l}
 (\neg q_{i+1} \vee \neg q_i) \\ 
 (q_i \vee q_{i+1}) \\
 (\neg p_{i+1} \vee \neg q_i \vee \neg p_i) \\
 (p_{i+1} \vee q_i \vee \neg p_i) \\
 (\neg p_{i+1} \vee q_i \vee p_i) \\
 (p_{i+1} \vee \neg q_i \vee p_i) 
\end{array}
$$
Ono što hoćemo da dokažemo da je $(p_0 \Leftrightarrow p_4) \wedge (q_0 \Leftrightarrow q_4)$ logička posledica
gornjih veza, tj. da je odgovarajuća implikacija tautologija. To možemo da dokažemo tako što ćemo pomoću
SAT solvera dokazati da je negacija te implikacije kontradikcija, a to je sledeća CNF formula:

$$
\begin{array}{l}
 (\neg q_1 \vee \neg q_0) \\ 
 (q_0 \vee q_1) \\
 (\neg p_1 \vee \neg q_0 \vee \neg p_0) \\
 (p_1 \vee q_0 \vee \neg p_0) \\
 (\neg p_1 \vee q_0 \vee p_0) \\
 (p_1 \vee \neg q_0 \vee p_0) \\
 (\neg q_2 \vee \neg q_1) \\
 (q_1 \vee q_2) \\
 (\neg p_2 \vee \neg q_1 \vee \neg p_1) \\
 (p_2 \vee q_1 \vee \neg p_1) \\
 (\neg p_2 \vee q_1 \vee p_1) \\
 (p_2 \vee \neg q_1 \vee p_1) \\
 (\neg q_3 \vee \neg q_2) \\
  (q_2 \vee q_3) \\
 (\neg p_3 \vee \neg q_2 \vee \neg p_2) \\
 (p_3 \vee q_2 \vee \neg p_2) \\
 (\neg p_3 \vee q_2 \vee p_2) \\
 (p_3 \vee \neg q_2 \vee p_2) \\
 (\neg q_4 \vee \neg q_3) \\ 
 (q_3 \vee q_4) \\
 (\neg p_4 \vee \neg q_3 \vee \neg p_3) \\
 (p_4 \vee q_3 \vee \neg p_3) \\
 (\neg p_4 \vee q_3 \vee p_3) \\
 (p_4 \vee \neg q_3 \vee p_3) \\
 (\neg p_0 \vee \neg p_4 \vee \neg q_0 \vee \neg q_4) \\
 (p_0 \vee  p_4 \vee \neg q_0 \vee \neg q_4) \\
 (\neg p_0 \vee \neg p_4 \vee  q_0 \vee  q_4) \\
 (p_0 \vee  p_4 \vee  q_0 \vee q_4) \\
\end{array}
$$

SAT rešavač MINISAT zaista potvrđuje da je ovaj skup klauza nezadovoljiv, tj. da je polazna implikacija
tautologija.


\end{solution}



\end{document}
