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$, $12\times6,$
  10                 $10\times7,$ $18\times5,$ $20\times4,$ $10\times6,$ $8\times6$ and
  11                 $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 component should
  15                 have at least one point in common with an edge of the power component.
  16         \item Due to limits on heat production the power components should be not too
  17                 close: their centres should differ at least $17$ in either the $x$
  18                 direction or the $y$ direction (or both).
  19 \end{itemize}
  20 }
  21
  22 \subsection{Formal definition}
  23 For every component $c$ for $i\in PC\cup RC$ where $PC=[01,02,03]$ and
  24 $RC=[04,05,06,07,08,09,10,11]$ we define a width, a height variable, an x and a
  25 y variable. $c_iw$, $c_ih$, $c_ix$ and $c_iy$. Although we call the height and
  26 width they represent just the sides since the components can be rotated. To
  27 represent this we introduce functions $h(c)$ and $w(c)$ that return the
  28 specified width and height.
  29
  30 \begin{align}
  31         \bigwedge_{i\in PC\cup RC}\Biggl(
  32           & (c_ih=h(i)\vee c_ih=w(i))\wedge(c_iw=w(i)\vee c_iw=h(i))\\
  33                 & \wedge 29-c_iw\geq c_ix>0\wedge 22-c_ih\geq c_iy>0\\
  34                 & \wedge \bigwedge_{j\in PC\cup RC}\Bigl(\\
  35                 \nonumber & \qquad\qquad\qquad j\geq i\\
  36                 \nonumber & \qquad\qquad\qquad \vee c_ix>c_jx+c_jw\\
  37                 \nonumber & \qquad\qquad\qquad \vee c_ix+c_jw<c_jx\\
  38                 \nonumber & \qquad\qquad\qquad \vee c_iy>c_jy+c_jh\\
  39                 \nonumber & \qquad\qquad\qquad \vee c_iy+c_jh<c_jh\Bigr)\Biggr)\wedge\\
  40         \bigwedge_{i\in PC}\bigwedge_{j\in PC}\Biggl( & i=j\\
  41                 \nonumber & \vee\frac{c_ix+c_iw}{2}-\frac{c_jx+c_jw}{2}>15\\
  42                 \nonumber & \vee\frac{c_jx+c_jw}{2}-\frac{c_ix+c_iw}{2}>15\\
  43                 \nonumber & \vee\frac{c_iy+c_ih}{2}-\frac{c_jy+c_jh}{2}>15\\
  44                 \nonumber & \vee\frac{c_jy+c_jh}{2}-\frac{c_iy+c_ih}{2}>15\Biggr)\wedge\\
  45         \bigwedge_{i\in RC}\bigvee_{j\in PC}\Biggl(
  46                 \nonumber & !(     c_ix-1     >c_jx+c_jw\\
  47                 \nonumber & \vee c_ix+1+c_jw<c_jx\\
  48                 \nonumber & \vee c_iy-1     >c_jy+c_jh\\
  49                 \nonumber & \vee c_iy+1+c_jh<c_jh\Biggr)\\
  50 \end{align}
  51
  52 \subsection{SMT format solution}