ChipDesign: a bit more final?

2 files changed, 192 insertions, 4 deletions

diff --git a/chip_design/solution-to-latex.py b/chip_design/solution-to-latex.py
index 6c74f4c..46cd838 100755
--- a/chip_design/solution-to-latex.py
+++ b/chip_design/solution-to-latex.py
@@ -8,6 +8,13 @@ import sys
 # Map component index to (x, y, width, height)
 boxes = {}
 
+# Reads input, line-by-line. Ignore the first line that just says "sat".
+# Other lines that are accepted:
+# x0 -> 2.0
+# y0 -> (/ 7.0 5.0)
+# w0 -> 3.0
+# h0 -> 4.0
+# Reads it into: boxes[0] = (x, y, width, height) = (2, 7/5, 3, 4)
 for line in sys.stdin:
     line = line.strip()
     if line == 'sat':
@@ -89,7 +96,7 @@ def print_boxes():
         x, y, w, h = component
         x2, y2 = x + w, y + h
 
-        # Draw number for debugging
+        # Draw number, coordinate and dimensions for debugging
         tx = x + w/2
         ty = y + h/2
         text = r"%s\\(%s,%s)\\(%s x %s)" % (i, x, y, w, h)
diff --git a/part1.tex b/part1.tex
index 75087b8..22e7ef3 100644
--- a/part1.tex
+++ b/part1.tex
@@ -7,6 +7,9 @@
 \usepackage{gensymb}
 \usepackage{listings}
 \usepackage{tikz}
+\usepackage{amsmath}
+\usepackage{hyperref}
+\usepackage{float}
 %\pagestyle{empty}
 \newcommand{\tr}{\mbox{\sf true}}
 \newcommand{\fa}{\mbox{\sf false}}
@@ -66,12 +69,185 @@ Give a chip design containing two power components and ten regular components sa
     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).
+their centres should differ at least 17 in either the $x$ direction or the $y$
+direction (or both).
 \end{itemize}
 
 \subsection*{Solution:}
-
+We generalize this problem to fitting $n \geq 1$ components on a chip with
+dimensions $w_c \times h_c$. Of these components, the first $1 \leq m < n$
+components are considered power components.
+For all components with index $0 \leq i < n$, a corner (the bottom-left one
+in a Cartesian space) is represented by $(x_i, y_i)$ and the dimensions are $w_i
+\times h_i$. (Observe that $(x_i + w_i, y_i + h_i)$ represents the opposite
+corner, for brevity we will write this as $(x'_i, y'_i)$.)
+
+To limit each component $i$ to the chip area:
+\begin{align}
+\label{eq:chip1}
+    \bigwedge_{i=0}^{n-1}
+    x_i \geq 0 \land y_i \geq 0 \land
+        x'_i \leq c_w \land y'_i \leq c_h
+\end{align}
+
+Each component has a given width $w'_i$ and height $h'_i$. To handle rotated
+components, we also allow these values to be swapped:
+\begin{align}
+\label{eq:chip2}
+    &\bigwedge_{i=0}^{n-1}
+    (w_i = w'_i \land h_i = h'_i) \lor (w_i = h'_i \land h_i = w'_i) \\
+    &= ((w_0 = 4 \land h_0 = 3) \lor
+       (w_0 = 3 \land h_0 = 4)) \nonumber \\
+    &\land ((w_1 = 4 \land h_1 = 3) \lor
+       (w_1 = 3 \land h_1 = 4)) \nonumber \\
+    &\land ((w_2 = 4 \land h_2 = 5) \lor
+       (w_2 = 5 \land h_2 = 4)) \nonumber \\
+    &\land \cdots \nonumber
+\end{align}
+
+To avoid an overlap between any pair of components $i$ and $j$ (with $i \neq
+j$), we add the restriction that each other component $j$ must be located either
+below, to the left, above or to the right of a component $i$.
+\begin{align}
+\label{eq:chip3}
+\bigwedge_{0 \leq i < n}
+\bigwedge_{0 \leq j < n, i \neq j}
+y'_j \leq y_i \lor
+x'_j \leq x_i \lor
+y_j \geq y'_i \lor
+x_j \geq x'_i
+\end{align}
+
+To ensure that a point on the edge of a power component matches with any of the
+four sides of a regular component, they must have the same $x$ coordinates (for
+the left and right sides) or the same $y$ coordinates (for the bottom and top
+side).  Besides having a shared axis, there must actual be an overlap with the
+$y$ or $x$ coordinates, respectively.
+
+Let $0 \leq i < m$ be the power component and $m \leq j < n$ be the regular
+component. Then each regular component $i$ must have a match with some power
+component $j$ (for clarity one part of the formula is split off):
+\begin{align}
+\label{eq:chip4}
+\bigwedge_{0 \leq i < m}
+\bigvee_{m \leq j < n}
+    (
+        (y'_j = y_i \lor y_j = y'_i)
+        \land hasOverlap_x(i, j)
+    ) \lor \nonumber \\ (
+        (x'_j = x_i \lor x_j = x'_i)
+        \land hasOverlap_y(i, j)
+    )
+\end{align}
+
+Now we define $hasOverlap_{axis}(i, j)$ which must detect the cases shown in
+Figure~\ref{fig:overlapCases} (for regular component $i$ and power component
+$j$).
+
+\begin{figure}[H]
+\centering
+\begin{tikzpicture}
+\draw[fill=red,red] (1,0) rectangle (3,.5);
+\draw (1,0) -- (1,.6);
+\draw (3,0) -- (3,.6);
+
+\node at (-.5,1) {\small{1}};
+\draw[dotted] (0,1) -- (.5,1);
+\draw[fill=white] (0,1) circle (0.1);
+\draw[fill=white] (.5,1) circle (0.1);
+
+\draw[dotted] (4,1) -- (4.5,1);
+\draw[fill=white] (4,1) circle (0.1);
+\draw[fill=white] (4.5,1) circle (0.1);
+
+\node at (-.5,1.5) {\small{2}};
+\draw[dotted] (0,1.5) -- (1,1.5);
+\draw (1,1.5) -- (2,1.5);
+\draw[fill=white] (0,1.5) circle (0.1);
+\draw[fill=black] (2,1.5) circle (0.1);
+
+\node at (-.5,2) {\small{3}};
+\draw (1.5,2) -- (2.5,2);
+\draw[fill=black] (1.5,2) circle (0.1);
+\draw[fill=black] (2.5,2) circle (0.1);
+
+\node at (-.5,2.5) {\small{4}};
+\draw (2,2.5) -- (3,2.5);
+\draw[dotted] (3,2.5) -- (4,2.5);
+\draw[fill=black] (2,2.5) circle (0.1);
+\draw[fill=white] (4,2.5) circle (0.1);
+
+\node at (-.5,3) {\small{5}};
+\draw[dotted] (.5,3) -- (1,3);
+\draw (1,3) -- (3,3);
+\draw[dotted] (3,3) -- (3.5,3);
+\draw[fill=white] (.5,3) circle (0.1);
+\draw[fill=white] (3.5,3) circle (0.1);
+\end{tikzpicture}
+\caption{\label{fig:overlapCases}
+Cases that are considered for overlap. The solid lines can be considered
+matching while the dotted part are not. The red rectangle on the bottom can be
+considered the power component while the lines on above represent the sides of
+regular components.}
+\end{figure}
+
+We are interested in the assignments that result in an overlap (that is,
+the cases having solid lines in the figure) and do a case distinction based on
+Figure~\ref{fig:overlapCases} for $axis=x$ (the same analysis applies to
+$axis=y$):
+\begin{enumerate}
+\item No overlap, the ends of the rectangle are not within any of the two lines.
+\item Overlap, the left end of the rectangle is within the ends of the line:
+    $x_i \leq x_j \land x_j \leq x'_i$.
+\item Overlap, both ends of the line are within the rectangle. To account for
+    this, it is sufficient to check just one end though. For the begin of the
+    line: $x_j \leq x_i \land x_i \leq x'_j$.
+\item Overlap, the right end of the rectangle is within the ends of the line:
+    $x_i \leq x'_j \land x'_j \leq x'_i$.
+\item Overlap, both the left and right ends of the rectangle are within the
+    begin and end of the line. Either check from (2) or (4) can be used here.
+\end{enumerate}
+
+(Note that in our case, the third check will never be satisfied since no side of
+a regular component is smaller than the smallest side power components and can
+therefore be removed. To generalize the following definition of $hasOverlap$,
+one should add this third condition to the conjunction though.)
+
+With the above analysis, we can define:
+\begin{align*}
+hasOverlap_x(i, j) &=
+(x_i \leq x_j  \land x_j  \leq x'_i) \lor
+(x_i \leq x'_j \land x'_j \leq x'_i) \\
+hasOverlap_y(i, j) &=
+(y_i \leq y_j  \land y_j  \leq y'_i) \lor
+(y_i \leq y'_j \land y'_j \leq y'_i)
+\end{align*}
+
+Finally we must add a clause that ensures a difference of at least
+$powerDistance$ between the centers of any pair of power components $i$, $j$
+(with $i \neq j$). (Note that this is a horizontal or vertical difference, not
+the Euclidean one.) Let the center for a power component $i$ be defined by:
+\begin{align*}
+cx_i &= x_i + \frac{1}{2}w_i &
+cy_i &= y_i + \frac{1}{2}h_i
+\end{align*}
+then:
+\begin{align}
+\label{eq:chip5}
+\bigwedge_{0 \leq i < m}
+\bigwedge_{0 \leq j < m, i \neq j}
+cx_i \geq& cx_j + powerDistance \lor
+cx_j \geq cx_i + powerDistance \lor \\
+cy_i \geq& cy_j + powerDistance \lor
+cy_j \geq cy_i + powerDistance
+\end{align}
+
+Taking the conjunction of the above parts (\ref{eq:chip1}, \ref{eq:chip2},
+\ref{eq:chip3}, \ref{eq:chip4}, \ref{eq:chip5}),
+we obtain a result which is visualized in Figure~\ref{fig:chipDesign}.
+
+\begin{figure}
+\centering
 \begin{tikzpicture}[scale=0.5]
 %\draw[step=1,gray,very thin] (0, 0) grid (30, 30);
 \draw[red,thick] (-.5, -.5) rectangle (30.5, 30.5);
@@ -101,6 +277,11 @@ their centres should differ at least 17 in either the x direction or the y direc
 \draw[draw=pink] (10.01, 14.01) rectangle (29.99, 23.99);
 \node[align=center] at (20.000000,19.000000) {11\\(10,14)\\(20 x 10)};
 \end{tikzpicture}
+\caption{\label{fig:chipDesign}Visualization of chip design satisfying the
+given requirements ($m=2$, $n=10$, $powerDistance=17$). The red boxes mark the
+power components. The component index is given, followed by the coordinate
+of the bottom-left corner and the dimension.}
+\end{figure}
 
 \section*{Problem: Job scheduling}
 Twelve jobs numbered from 1 to 12 have to be executed satisfying the following requirements: