update

[master.git] / ar / assignments / 2.tex

diff --git a/ar/assignments/2.tex b/ar/assignments/2.tex
index e69de29..d1b13f1 100644 (file)
--- a/ar/assignments/2.tex
+++ b/ar/assignments/2.tex
@@ -0,0 +1,51 @@
+\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}
+}
+
+\subsection{Formal definition}
+For every component $c$ for $i\in PC\cup RC$ where $PC=[01,02,03]$ and
+$RC=[04,05,06,07,08,09,10,11]$ we define a width, a height variable, an x and a
+y variable. $c_iw$, $c_ih$, $c_ix$ and $c_iy$. Although we call the height and
+width they represent just the sides since the components can be rotated. To
+represent this we introduce functions $h(c)$ and $w(c)$ that return the
+specified width and height.
+
+\begin{align}
+       \bigwedge_{i\in PC\cup RC}\Biggl(
+         & (c_ih=h(i)\vee c_ih=w(i))\wedge(c_iw=w(i)\vee c_iw=h(i))\\
+               & \wedge 29-c_iw\geq c_ix>0\wedge 22-c_ih\geq c_iy>0\\
+               & \wedge \bigwedge_{j\in PC\cup RC}\Bigl(\\
+               \nonumber & \qquad\qquad\qquad j\geq i\\
+               \nonumber & \qquad\qquad\qquad \vee c_ix>c_jx+c_jw\\
+               \nonumber & \qquad\qquad\qquad \vee c_ix+c_jw<c_jx\\
+               \nonumber & \qquad\qquad\qquad \vee c_iy>c_jy+c_jh\\
+               \nonumber & \qquad\qquad\qquad \vee c_iy+c_jh<c_jh\Bigr)\Biggr)\wedge\\
+       \bigwedge_{i\in PC}\bigwedge_{j\in PC}\Biggl( & i=j\\
+               \nonumber & \vee\frac{c_ix+c_iw}{2}-\frac{c_jx+c_jw}{2}>15\\
+               \nonumber & \vee\frac{c_jx+c_jw}{2}-\frac{c_ix+c_iw}{2}>15\\
+               \nonumber & \vee\frac{c_iy+c_ih}{2}-\frac{c_jy+c_jh}{2}>15\\
+               \nonumber & \vee\frac{c_jy+c_jh}{2}-\frac{c_iy+c_ih}{2}>15\Biggr)\wedge\\
+       \bigwedge_{i\in RC}\bigvee_{j\in PC}\Biggl( & c_ix=c_jx+c_jw+1\\
+               \nonumber & \vee c_ix+c_iw+1=c_jx\\
+               \nonumber & \vee c_iy=c_jy+c_jh+1\\
+               \nonumber & \vee c_iy+c_ih+1=c_jy\Biggr)
+\end{align}
+
+\subsection{SMT format solution}