update report, added solution to 2 image

[master.git] / ar / assignments / 2.tex

diff --git a/ar/assignments/2.tex b/ar/assignments/2.tex
index 7bd482d..f4789d8 100644 (file)
--- a/ar/assignments/2.tex
+++ b/ar/assignments/2.tex
@@ -38,10 +38,10 @@ specified width and height.
                \nonumber & \qquad\qquad\qquad \vee c_iy>c_jy+c_jh\\
                \nonumber & \qquad\qquad\qquad \vee c_iy+c_jh<c_jh\Bigr)\Biggr)\wedge\\
        \bigwedge_{i\in PC}\bigwedge_{j\in PC}\Biggl( & i=j\\
-               \nonumber & \vee c_ix+\frac{c_iw}{2}-c_jx+\frac{c_jw}{2}>15\\
-               \nonumber & \vee c_jx+\frac{c_jw}{2}-c_ix+\frac{c_iw}{2}>15\\
-               \nonumber & \vee c_iy+\frac{c_ih}{2}-c_jy+\frac{c_jh}{2}>15\\
-               \nonumber & \vee c_jy+\frac{c_jh}{2}-c_iy+\frac{c_ih}{2}>15\Biggr)\wedge\\
+               \nonumber & \vee c_ix+\frac{c_iw}{2}-c_jx+\frac{c_jw}{2}>17\\
+               \nonumber & \vee c_jx+\frac{c_jw}{2}-c_ix+\frac{c_iw}{2}>17\\
+               \nonumber & \vee c_iy+\frac{c_ih}{2}-c_jy+\frac{c_jh}{2}>17\\
+               \nonumber & \vee c_jy+\frac{c_jh}{2}-c_iy+\frac{c_ih}{2}>17\Biggr)\wedge\\
        \bigwedge_{i\in RC}\bigvee_{j\in PC}\neg\Biggl(
                & (c_ix-1>c_jx+c_jw\\
                \nonumber & \vee c_ix+1+c_jw<c_jx\\
@@ -49,4 +49,54 @@ specified width and height.
                \nonumber & \vee c_iy+1+c_jh<c_jh\Biggr)
 \end{align}
 
+All subformulas describe a constraint from the problem description and can be
+separated in three groups. Subformulas going over all components, only power
+components and only regular components.
+\begin{itemize}
+       \item\textbf{All}
+               \begin{enumerate}
+                               \setcounter{enumi}{7}
+                       \item Describes that the width and the height of the component can be
+                               swapped(in case of rotation).
+                       \item Constrains location of the components in regard to the size of
+                               the chip.
+                       \item Makes sure the components do not overlap by defining for all
+                               pairs of components that they either are strictly right, strictly
+                               left, strictly above or strictly below the other.
+               \end{enumerate}
+       \item\textbf{Power only}
+               \begin{enumerate}
+                               \setcounter{enumi}{10}
+                               \item Power components must be at least $17$ block away from
+                                       other power components. This is defined by saying that the
+                                       difference between the center of each pair of components is
+                                       bigger then $17$.
+               \end{enumerate}
+       \item\textbf{Regular only}
+               \begin{enumerate}
+                               \setcounter{enumi}{11}
+                               \item Regular components must be connected to a power
+                                               components. This is described using the method from the
+                                               overalap calculation in a negated way. Every regular
+                                               component must have overlap with a power component that
+                                               has been enlarged by $1$.
+               \end{enumerate}
+\end{itemize}
+
 \subsection{SMT format solution}
+The formula is easily convertable via a Python script to SMT format and said
+script is listed in Listing~\ref{listing:2.py}. The Python script optimizes a
+little bit from the original formula by leaving out the overlap checking
+between the same components. When we run the file a solution is found within
+$30$ seconds.
+
+\subsection{Solution}
+Figure~\ref{fig:s2} shows the configuration found by the solver. Light gray
+components are regular components and darker gray components are power
+components.
+
+\begin{figure}[H]
+       \includegraphics[scale=0.75]{s2.png}
+       \label{fig:s2}
+       \caption{Solution visualization for problem 2}
+\end{figure}