\begin{itemize}
\item The width of the chip is 29 and the height is 22.
\item All power components have width 4 and height 2.
- \item The sizes of the eight regular components are $9\times7$, $12\times6,$
- $10\times7,$ $18\times5,$ $20\times4,$ $10\times6,$ $8\times6$ and
- $10\times8$ respectively.
+ \item The sizes of the eight regular components are $9\times7$,
+ $12\times6,$ $10\times7,$ $18\times5,$ $20\times4,$
+ $10\times6,$ $8\times6$ and $10\times8$ respectively.
\item All components may be turned 90, but may not overlap.
\item In order to get power, all regular components should directly be
- connected to a power component, that is, an edge of the component should
- have at least one point in common with an edge of the power component.
- \item Due to limits on heat production the power components should be not too
- close: their centres should differ at least $17$ in either the $x$
- direction or the $y$ direction (or both).
+ connected to a power component, that is, an edge of the
+ component should have at least one point in common with an edge
+ of the power component.
+ \item Due to limits on heat production the power components should be
+ not too close: their centres should differ at least $17$ in
+ either the $x$ direction or the $y$ direction (or both).
\end{itemize}
}
+\newpage
\subsection{Formal definition}
-For every component $c$ for $i\in PC\cup RC$ where $PC=[01,02,03]$ and
-$RC=[04,05,06,07,08,09,10,11]$ we define a width, a height variable, an x and a
-y variable. $c_iw$, $c_ih$, $c_ix$ and $c_iy$. Although we call the height and
-width they represent just the sides since the components can be rotated. To
-represent this we introduce functions $h(c)$ and $w(c)$ that return the
-specified width and height.
+For every component $c_{i}$ for $i\in PC\cup RC$ where $PC=\{1,\ldots,3\}$ and
+$RC=\{4,\ldots,11\}$ we define a width, a height, an $x$ and a $y$ variables
+$c_{i}w$, $c_{i}h$, $c_{i}x$ and $c_{i}y$. $c_ih$ does not necessarily have the
+specified height of the components since the components may be rotated. For the
+specified width and height we introduce the functions $h(c)$ and $w(c)$ that
+return the specified width and height.
+
+This leads to the following formalization.
\begin{align}
\bigwedge_{i\in PC\cup RC}\Biggl(
- & (c_ih=h(i)\vee c_ih=w(i))\wedge(c_iw=w(i)\vee c_iw=h(i))\\
- & \wedge 29-c_iw\geq c_ix>0\wedge 22-c_ih\geq c_iy>0\\
- & \wedge \bigwedge_{j\in PC\cup RC}\Bigl(\\
- \nonumber & \qquad\qquad\qquad j\geq i\\
- \nonumber & \qquad\qquad\qquad \vee c_ix>c_jx+c_jw\\
- \nonumber & \qquad\qquad\qquad \vee c_ix+c_jw<c_jx\\
- \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\\
+ & (c_{i}h=h(i)\vee c_{i}h=w(i))\wedge(c_{i}w=w(i)\vee c_{i}w=h(i))\\
+ & \wedge 29-c_{i}w\geq c_{i}x>0\wedge 22-c_{i}h\geq c_{i}y>0\\
+ & \wedge \bigwedge_{j\in PC\cup RC}\Bigl(j\geq i\\
+ \nonumber & \qquad\qquad\qquad \vee c_{i}x>c_{j}x+c_{j}w\\
+ \nonumber & \qquad\qquad\qquad \vee c_{i}x+c_{j}w<c_{j}x\\
+ \nonumber & \qquad\qquad\qquad \vee c_{i}y>c_{j}y+c_{j}h\\
+ \nonumber & \qquad\qquad\qquad
+ \vee c_{i}y+c_{j}h<c_{j}h\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}>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\\
+ \nonumber & \vee c_{i}x+\nicefrac{c_{i}w}{2}-
+ c_{j}x+\nicefrac{c_{j}w}{2}>17\\
+ \nonumber & \vee c_{j}x+\nicefrac{c_{j}w}{2}-
+ c_{i}x+\nicefrac{c_{i}w}{2}>17\\
+ \nonumber & \vee c_{i}y+\nicefrac{c_{i}h}{2}-
+ c_{j}y+\nicefrac{c_{j}h}{2}>17\\
+ \nonumber & \vee c_{j}y+\nicefrac{c_{j}h}{2}-
+ c_{i}y+\nicefrac{c_{i}h}{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\\
- \nonumber & \vee c_iy-1>c_jy+c_jh\\
- \nonumber & \vee c_iy+1+c_jh<c_jh\Biggr)
+ & (c_{i}x-1>c_{j}x+c_{j}w\\
+ \nonumber & \vee c_{i}x+1+c_{j}w<c_{j}x\\
+ \nonumber & \vee c_{i}y-1>c_{j}y+c_{j}h\\
+ \nonumber & \vee c_{i}y+1+c_{j}h<c_{j}h\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.
+Every numbered subformula describes a constraint from the problem description.
+We can separated the subformulas in formulas 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.
+ \setcounter{enumi}{7}
+ \item Makes sure the width and the height of the
+ component can be swapped thus allowing a
+ rotation.
+ \item Makes sure the components are placed on the
+ chip by stating that the $x$ and $y$
+ coordinates are bigger then $0$ and the $x$ and
+ $y$ plus their width or height does not exceed
+ the specified width and height 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$.
+ \setcounter{enumi}{10}
+ \item Makes sure power components are at least $17$
+ block away from other power components by
+ stating 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$.
+ \setcounter{enumi}{11}
+ \item Makes sure regular components are connected to a
+ power component by stating, using the same
+ method as in the overlay, that it has overlap
+ with a power component that has had its size
+ increased 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
+script is listed in Listing~\ref{listing:a2.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.
+between the same components. The solution is calculated using the command shown
+in Listing~\ref{listing:2.bash}
+
+\lstinputlisting[language=bash,
+ caption={Find the shortest solution for problem 3},
+ label={listing:2.bash}]{src/a2.bash}
\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.
+Finding this solution takes less then $35$ seconds and is shown in
+Figure~\ref{fig:s2}.
+
+Light gray blocks represent regular components and the darker gray
+blocks represent power components.
\begin{figure}[H]
- \includegraphics[scale=0.75]{s2.png}
- \label{fig:s2}
+ \includegraphics[scale=0.70]{s2.png}
+\label{fig:s2}
\caption{Solution visualization for problem 2}
\end{figure}
repositories / master.git / blobdiff