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 by literal
 101 conversion and said script is listed in Listing~\ref{listing:a2.bash}. The
 102 script optimizes a little bit from the original formula by leaving out the
 103 overlap checking between the same components. The solution is calculated using
 104 the command shown in Listing~\ref{listing:2.bash} and visualized with the
 105 python script shown in Listing~\ref{listing:a2.py}
 106
 107 \lstinputlisting[language=bash,
 108         caption={Find the shortest solution for problem 3},
 109         label={listing:2.bash}]{src/a2.bash}
 110
 111 \subsection{Solution}
 112 Finding this solution takes less then $35$ seconds and is shown in
 113 Table~\ref{tab:s2}.
 114
 115 The bold items represent the power components.
 116
 117 \begin{table}[H]
 118         \centering
 119         \input{a2.tex}
 120 \label{tab:s2}
 121         \caption{Solution visualization for problem 2}
 122 \end{table}