+++ /dev/null
-\section{Problem 2}
-{\em
- Give a chip design containing three power components and eight regular
-components satisfying the following constraints:
-
-\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 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).
-\end{itemize}
-}
-
-\newpage
-\subsection{Formal definition}
-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_{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_{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_{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}
-
-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 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 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 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:a2.py}. The Python script optimizes a
-little bit from the original formula by leaving out the overlap checking
-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}
-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.70]{s2.png}
-\label{fig:s2}
- \caption{Solution visualization for problem 2}
-\end{figure}
repositories / master.git / blobdiff