ar/assignments/2.tex

   1 \section{Problem 2}
   2 {\em
   3  Give a chip design containing three power components and eight regular
   4 components satisfying the following constraints:
   5
   6 \begin{itemize}
   7         \item The width of the chip is 29 and the height is 22.
   8         \item All power components have width 4 and height 2.
   9         \item The sizes of the eight regular components are $9\times7$,
  10                 $12\times6,$ $10\times7,$ $18\times5,$ $20\times4,$
  11                 $10\times6,$ $8\times6$ and $10\times8$ respectively.
  12         \item All components may be turned 90, but may not overlap.
  13         \item In order to get power, all regular components should directly be
  14                 connected to a power component, that is, an edge of the
  15                 component should have at least one point in common with an edge
  16                 of the power component.
  17         \item Due to limits on heat production the power components should be
  18                 not too close: their centres should differ at least $17$ in
  19                 either the $x$ direction or the $y$ direction (or both).
  20 \end{itemize}
  21 }
  22
  23 \newpage
  24 \subsection{Formal definition}
  25 For every component $c_{i}$ for $i\in PC\cup RC$ where $PC=\{1,\ldots,3\}$ and
  26 $RC=\{4,\ldots,11\}$ we define a width, a height, an $x$ and a $y$ variables
  27 $c_{i}w$, $c_{i}h$, $c_{i}x$ and $c_{i}y$. $c_ih$ does not necessarily have the
  28 specified height of the components since the components may be rotated. For the
  29 specified width and height we introduce the functions $h(c)$ and $w(c)$ that
  30 return the specified width and height.
  31
  32 This leads to the following formalization.
  33
  34 \begin{align}
  35         \bigwedge_{i\in PC\cup RC}\Biggl(
  36           & (c_{i}h=h(i)\vee c_{i}h=w(i))\wedge(c_{i}w=w(i)\vee c_{i}w=h(i))\\
  37                 & \wedge 29-c_{i}w\geq c_{i}x>0\wedge 22-c_{i}h\geq c_{i}y>0\\
  38                 & \wedge \bigwedge_{j\in PC\cup RC}\Bigl(j\geq i\\
  39                 \nonumber & \qquad\qquad\qquad \vee c_{i}x>c_{j}x+c_{j}w\\
  40                 \nonumber & \qquad\qquad\qquad \vee c_{i}x+c_{j}w<c_{j}x\\
  41                 \nonumber & \qquad\qquad\qquad \vee c_{i}y>c_{j}y+c_{j}h\\
  42                 \nonumber & \qquad\qquad\qquad
  43                         \vee c_{i}y+c_{j}h<c_{j}h\Bigr)\Biggr)\wedge\\
  44         \bigwedge_{i\in PC}\bigwedge_{j\in PC}\Biggl( & i=j\\
  45                 \nonumber & \vee c_{i}x+\nicefrac{c_{i}w}{2}-
  46                         c_{j}x+\nicefrac{c_{j}w}{2}>17\\
  47                 \nonumber & \vee c_{j}x+\nicefrac{c_{j}w}{2}-
  48                         c_{i}x+\nicefrac{c_{i}w}{2}>17\\
  49                 \nonumber & \vee c_{i}y+\nicefrac{c_{i}h}{2}-
  50                         c_{j}y+\nicefrac{c_{j}h}{2}>17\\
  51                 \nonumber & \vee c_{j}y+\nicefrac{c_{j}h}{2}-
  52                         c_{i}y+\nicefrac{c_{i}h}{2}>17\Biggr)\wedge\\
  53         \bigwedge_{i\in RC}\bigvee_{j\in PC}\neg\Biggl(
  54                 & (c_{i}x-1>c_{j}x+c_{j}w\\
  55                 \nonumber & \vee c_{i}x+1+c_{j}w<c_{j}x\\
  56                 \nonumber & \vee c_{i}y-1>c_{j}y+c_{j}h\\
  57                 \nonumber & \vee c_{i}y+1+c_{j}h<c_{j}h\Biggr)
  58 \end{align}
  59
  60 Every numbered subformula describes a constraint from the problem description.
  61 We can separated the subformulas in formulas going over all components, only
  62 power components and only regular components.
  63 \begin{itemize}
  64         \item\textbf{All}
  65                 \begin{enumerate}
  66                         \setcounter{enumi}{7}
  67                         \item Makes sure the width and the height of the
  68                                 component can be swapped thus allowing a
  69                                 rotation.
  70                         \item Makes sure the components are placed on the
  71                                 chip by stating that the $x$ and $y$
  72                                 coordinates are bigger then $0$ and the $x$ and
  73                                 $y$ plus their width or height does not exceed
  74                                 the specified width and height of the chip.
  75                         \item Makes sure the components do not overlap by
  76                                 defining for all pairs of components that they
  77                                 either are strictly right, strictly left,
  78                                 strictly above or strictly below the other.
  79                 \end{enumerate}
  80         \item\textbf{Power only}
  81                 \begin{enumerate}
  82                         \setcounter{enumi}{10}
  83                         \item Makes sure power components are at least $17$
  84                                 block away from other power components by
  85                                 stating that the difference between the center
  86                                 of each pair of components is bigger then $17$.
  87                 \end{enumerate}
  88         \item\textbf{Regular only}
  89                 \begin{enumerate}
  90                         \setcounter{enumi}{11}
  91                         \item Makes sure regular components are connected to a
  92                                 power component by stating, using the same
  93                                 method as in the overlay, that it has overlap
  94                                 with a power component that has had its size
  95                                 increased by $1$.
  96                 \end{enumerate}
  97 \end{itemize}
  98
  99 \subsection{SMT format solution}
 100 The formula is easily convertable via a Python script to SMT format and said
 101 script is listed in Listing~\ref{listing:a2.py}. The Python script optimizes a
 102 little bit from the original formula by leaving out the overlap checking
 103 between the same components. The solution is calculated using the command shown
 104 in Listing~\ref{listing:2.bash}
 105
 106 \lstinputlisting[language=bash,
 107         caption={Find the shortest solution for problem 3},
 108         label={listing:2.bash}]{src/a2.bash}
 109
 110 \subsection{Solution}
 111 Finding this solution takes less then $35$ seconds and is shown in
 112 Figure~\ref{fig:s2}.
 113
 114 Light gray blocks represent regular components and the darker gray
 115 blocks represent power components.
 116
 117 \begin{figure}[H]
 118         \includegraphics[scale=0.70]{s2.png}
 119 \label{fig:s2}
 120         \caption{Solution visualization for problem 2}
 121 \end{figure}