a1/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 \subsection{Formal definition}
  24 For every component $c_{i}$ for $i\in PC\cup RC$ where $PC=\{1,\ldots,3\}$ and
  25 $RC=\{4,\ldots,11\}$ we define a width, a height, an $x$ and a $y$ variables
  26 $c_{i}w$, $c_{i}h$, $c_{i}x$ and $c_{i}y$. $c_ih$ does not necessarily have the
  27 specified height of the components since the components may be rotated. For the
  28 specified width and height we introduce the functions $h(c)$ and $w(c)$ that
  29 return the specified width and height.
  30
  31 This leads to the following formalization.
  32
  33 \begin{align}
  34         \bigwedge_{i\in PC\cup RC}\Biggl(
  35           & (c_{i}h=h(i)\vee c_{i}h=w(i))\wedge(c_{i}w=w(i)\vee c_{i}w=h(i))\\
  36                 & \wedge 29-c_{i}w\geq c_{i}x>0\wedge 22-c_{i}h\geq c_{i}y>0\\
  37                 & \wedge \bigwedge_{j\in PC\cup RC}\Bigl(j\geq i\\
  38                 \nonumber & \qquad\qquad\qquad \vee c_{i}x>c_{j}x+c_{j}w\\
  39                 \nonumber & \qquad\qquad\qquad \vee c_{i}x+c_{j}w<c_{j}x\\
  40                 \nonumber & \qquad\qquad\qquad \vee c_{i}y>c_{j}y+c_{j}h\\
  41                 \nonumber & \qquad\qquad\qquad
  42                         \vee c_{i}y+c_{j}h<c_{j}h\Bigr)\Biggr)\wedge\\
  43         \bigwedge_{i\in PC}\bigwedge_{j\in PC}\Biggl( & i=j\\
  44                 \nonumber & \vee c_{i}x+\nicefrac{c_{i}w}{2}-
  45                         c_{j}x+\nicefrac{c_{j}w}{2}>17\\
  46                 \nonumber & \vee c_{j}x+\nicefrac{c_{j}w}{2}-
  47                         c_{i}x+\nicefrac{c_{i}w}{2}>17\\
  48                 \nonumber & \vee c_{i}y+\nicefrac{c_{i}h}{2}-
  49                         c_{j}y+\nicefrac{c_{j}h}{2}>17\\
  50                 \nonumber & \vee c_{j}y+\nicefrac{c_{j}h}{2}-
  51                         c_{i}y+\nicefrac{c_{i}h}{2}>17\Biggr)\wedge\\
  52         \bigwedge_{i\in RC}\bigvee_{j\in PC}\neg\Biggl(
  53                 & (c_{i}x-1>c_{j}x+c_{j}w\\
  54                 \nonumber & \vee c_{i}x+1+c_{j}w<c_{j}x\\
  55                 \nonumber & \vee c_{i}y-1>c_{j}y+c_{j}h\\
  56                 \nonumber & \vee c_{i}y+1+c_{j}h<c_{j}h\Biggr)
  57 \end{align}
  58
  59 Every numbered subformula describes a constraint from the problem description.
  60 We can separated the subformulas in formulas going over all components, only
  61 power components and only regular components.
  62 \begin{itemize}
  63         \item\textbf{All}
  64                 \begin{enumerate}
  65                         \setcounter{enumi}{7}
  66                         \item Makes sure the width and the height of the
  67                                 component can be swapped thus allowing a
  68                                 rotation.
  69                         \item Makes sure the components are placed on the
  70                                 chip by stating that the $x$ and $y$
  71                                 coordinates are bigger then $0$ and the $x$ and
  72                                 $y$ plus their width or height does not exceed
  73                                 the specified width and height of the chip.
  74                         \item Makes sure the components do not overlap by
  75                                 defining for all pairs of components that they
  76                                 either are strictly right, strictly left,
  77                                 strictly above or strictly below the other.
  78                 \end{enumerate}
  79         \item\textbf{Power only}
  80                 \begin{enumerate}
  81                         \setcounter{enumi}{10}
  82                         \item Makes sure power components are at least $17$
  83                                 block away from other power components by
  84                                 stating that the difference between the center
  85                                 of each pair of components is bigger then $17$.
  86                 \end{enumerate}
  87         \item\textbf{Regular only}
  88                 \begin{enumerate}
  89                         \setcounter{enumi}{11}
  90                         \item Makes sure regular components are connected to a
  91                                 power component by stating, using the same
  92                                 method as in the overlay, that it has overlap
  93                                 with a power component that has had its size
  94                                 increased by $1$.
  95                 \end{enumerate}
  96 \end{itemize}
  97
  98 \subsection{SMT format solution}
  99 The formula is easily convertable via a script to SMT format by literal
 100 conversion. The script optimizes a little bit from the original formula by
 101 leaving out the overlap checking between the same components.
 102
 103 \subsection{Solution}
 104 Finding this solution takes less then $35$ seconds and is shown in
 105 Table~\ref{tab:s2}.
 106
 107 The bold items represent the power components.
 108
 109 \begin{table}[H]
 110         \centering
 111         \input{a2.tex}
 112 \label{tab:s2}
 113         \caption{Solution visualization for problem 2}
 114 \end{table}