From ef9860fec9077d0be59cf0cf2c687b0ef51ffefe Mon Sep 17 00:00:00 2001
From: Peter Wu <peter@lekensteyn.nl>
Date: Tue, 13 Dec 2016 01:26:31 +0100
Subject: ChipDesign: optimize, finish report part

---
 chip_design/generate-chipdesign.py |  8 ++---
 part1.tex                          | 60 +++++++++++++++++++++++++++++++-------
 2 files changed, 52 insertions(+), 16 deletions(-)

diff --git a/chip_design/generate-chipdesign.py b/chip_design/generate-chipdesign.py
index ca2f229..bd96543 100755
--- a/chip_design/generate-chipdesign.py
+++ b/chip_design/generate-chipdesign.py
@@ -71,9 +71,7 @@ for i, (w, h) in enumerate(all_components):
 # Avoid overlap between any pair, so any other component must be outside the
 # current pivot.
 for i in range(len(all_components)):
-    for j in range(len(all_components)):
-        if i == j:
-            continue
+    for j in range(i + 1, len(all_components)):
         # other (j) must be below, on the left of pivot (i).
         # or above or on the right (mind the width/height!).
         altpreds = [
@@ -86,9 +84,7 @@ for i in range(len(all_components)):
 
 # require minimum distance between power components
 for i in range(len(powers)):
-    for j in range(len(powers)):
-        if i == j:
-            continue
+    for j in range(i + 1, len(powers)):
         # need center_i >= center_j + distance (for center from {X,Y}, repeat
         # for i and j swapped in case j occurs after i)
         # center = x + w / 2
diff --git a/part1.tex b/part1.tex
index 22e7ef3..f92fb70 100644
--- a/part1.tex
+++ b/part1.tex
@@ -105,13 +105,15 @@ components, we also allow these values to be swapped:
     &\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$.
+To avoid an overlap between any pair of components $i$ and $j$ (with $i < 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$. (Note the use of
+$i < j$ is sufficient, $i \neq j$ would also have been correct, but due to
+symmetry of the overlap check it would contain redundant parts.)
 \begin{align}
 \label{eq:chip3}
 \bigwedge_{0 \leq i < n}
-\bigwedge_{0 \leq j < n, i \neq j}
+\bigwedge_{i < j < n}
 y'_j \leq y_i \lor
 x'_j \leq x_i \lor
 y_j \geq y'_i \lor
@@ -225,26 +227,64 @@ hasOverlap_y(i, j) &=
 
 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
+(with $i < 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:
+then we have to check pairs that we have not seen yet:
 \begin{align}
 \label{eq:chip5}
 \bigwedge_{0 \leq i < m}
-\bigwedge_{0 \leq j < m, i \neq j}
+\bigwedge_{i < j < m}
 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}.
+We wrote a generator program that takes the conjunction of the above parts
+(formulae \ref{eq:chip1}, \ref{eq:chip2}, \ref{eq:chip3}, \ref{eq:chip4},
+\ref{eq:chip5}). Its annotated (partial) output is shown in
+Listing~\ref{lst:chipDesign}. Evaluation of this output using
+\texttt{python generate-chipdesign.py | z3 -smt -in} finished in 12 seconds.
+The result is visualized in Figure~\ref{fig:chipDesign}.
+Indeed, the requirements are satisfied.
+
+\begin{lstlisting}[caption={Generated SMT output for
+ChipDesign},label={lst:chipDesign},language=lisp,basicstyle=\scriptsize]
+(benchmark test.smt
+:logic QF_UFLIA
+:extrafuns ((x0 Int) (y0 Int) (w0 Int) (h0 Int) ...
+(x11 Int) (y11 Int) (w11 Int) (h11 Int))
+:formula (and
+; check requirement 1 (chip width and height)
+(>= x0 0) (>= y0 0) (<= (+ x0 w0) 30) (<= (+ y0 h0) 30)
+; check requirement 2 or 3 (component width)
+(or (and (= w0 4) (= h0 3)) (and (= w0 3) (= h0 4)))
+...
+(>= x11 0) (>= y11 0) (<= (+ x11 w11) 30) (<= (+ y11 h11) 30)
+(or (and (= w11 10) (= h11 20)) (and (= w11 20) (= h11 10)))
+; check requirement 4 (no overlap, may be turned)
+(or (<= (+ y1 h1) y0) (<= (+ x1 w1) x0)
+    (>= y1 (+ y0 h0)) (>= x1 (+ x0 w0)))
+...
+(or (<= (+ y11 h11) y10) (<= (+ x11 w11) x10)
+    (>= y11 (+ y10 h10)) (>= x11 (+ x10 w10)))
+; check requirement 6 (minimum distance between power components)
+(or (>= (+ x0 (/ w0 2)) (+ (+ x1 (/ w1 2)) 17))
+    ...
+)
+; check requirement 5 (power for regular components)
+(or (and
+      (or (= (+ y0 h0) y2) (= y0 (+ y2 h2)))
+      (or (and (<= x2 x0) (<= x0 (+ x2 w2)))
+          (and (<= x2 (+ x0 w0)) (<= (+ x0 w0) (+ x2 w2)))
+    ))
+    ...
+)...))
+\end{lstlisting}
 
 \begin{figure}
 \centering
-- 
cgit v1.2.1