1.1 --- a/exercises/solutions/sol04.tex	Thu May 31 01:17:45 2012 +0200
     1.2 +++ b/exercises/solutions/sol04.tex	Thu May 31 04:12:51 2012 +0200
     1.3 @@ -20,6 +20,7 @@
     1.4  \renewcommand{\familydefault}{\sfdefault}
     1.5  \newcommand{\R}{\mathcal{R}}
     1.6  \newcommand{\N}{\mathbb{N}}
     1.7 +\newcommand{\C}{\mathcal{C}}
     1.8  
     1.9  %\include{pythonlisting}
    1.10  
    1.11 @@ -166,5 +167,13 @@
    1.12        \{1, 2, 3, 4, 5\} & otherwise\\
    1.13      \end{array} \right.\\
    1.14  \end{align*}
    1.15 -That makes 32 domain values less and one hour less of my life. My solver spent full 1.5ms on this task. I'm glad we have the power to build machines for doing such tedious work instead of doing it by hand.
    1.16 +That makes 32 domain values less. I've spent an hour and this, where my solver spent 1.5ms on this task. I'm glad we have the power to build machines for doing such tedious work instead of doing it by hand.
    1.17 +
    1.18 +\section*{Exercise 4.2}
    1.19 +(a) We show that $Sol(\C) = Sol(\C')$ by contradiction.
    1.20 +
    1.21 +Let $\C=\langle V,D,C\rangle$ and $\C'=\langle V,D',C\rangle$. By definition each variable assignment $a(v_i)$ must be in its variable domain $D_i$, i.e., $a(v_i)\in D_i$. Therefore, a reduction of domains can only yield a network with less solutions. Since AC3 reduces domains, there can not be more solutions for $\C'$, i.e., $Sol(\C') \subseteq Sol(\C)$.
    1.22 +
    1.23 +Assume that solution $a\in Sol(\C)$ is lost after the domain reduction by AC3, i.e., $a\notin Sol(\C')$. WLOG it follows that at some iteration of AC3 the value $a(v_i)$ was removed from the domain $D_i'$, so it holds $a(v_i)\notin D_i'$. By the definition of the revise function of AC3, it holds that $D_i'\leftarrow D_i\cap\pi_i(R_{ij} \bowtie D_j)$. Since $a(v_i)$ is in $D_i$ but not in $D_i'$, it follows that $a(v_i)\notin\pi_i(R_{ij}\bowtie D_j) \implies (a(v_i),a(v_j))\notin(R_{ij}\bowtie D_j)$. The join $R_{ij}\bowtie D_j$ represents the set of all consistent assignments of variable $v_j$ over the relation $R_{ij}$. With $(a(v_i),a(v_j))\notin (R_{ij}\bowtie D_j)$ it follows that variable assignments $(a(v_i),a(v_j))$ are not consistent with the constraint over $R_{ij}$. It contradicts with our assumption that $a\in Sol(\C)$, because a solution must satisfy all constraints of the network. We have shown that there is no solution $a\in Sol(\C)$, such that $a\notin Sol(\C')$. \qed\\\\
    1.24 +(b) 
    1.25  \end{document}