From: Mart Lubbers <mart@martlubbers.net>
Date: Tue, 20 Oct 2015 18:21:47 +0000 (+0200)
Subject: update report, added solution to 2 image
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=931351f869d0197c78ac85ba4ba7718525969dc3;p=master.git

update report, added solution to 2 image
---

diff --git a/ar/assignments/2.tex b/ar/assignments/2.tex
index 7bd482d..f4789d8 100644
--- a/ar/assignments/2.tex
+++ b/ar/assignments/2.tex
@@ -38,10 +38,10 @@ specified width and height.
 		\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 c_ix+\frac{c_iw}{2}-c_jx+\frac{c_jw}{2}>15\\
-		\nonumber & \vee c_jx+\frac{c_jw}{2}-c_ix+\frac{c_iw}{2}>15\\
-		\nonumber & \vee c_iy+\frac{c_ih}{2}-c_jy+\frac{c_jh}{2}>15\\
-		\nonumber & \vee c_jy+\frac{c_jh}{2}-c_iy+\frac{c_ih}{2}>15\Biggr)\wedge\\
+		\nonumber & \vee c_ix+\frac{c_iw}{2}-c_jx+\frac{c_jw}{2}>17\\
+		\nonumber & \vee c_jx+\frac{c_jw}{2}-c_ix+\frac{c_iw}{2}>17\\
+		\nonumber & \vee c_iy+\frac{c_ih}{2}-c_jy+\frac{c_jh}{2}>17\\
+		\nonumber & \vee c_jy+\frac{c_jh}{2}-c_iy+\frac{c_ih}{2}>17\Biggr)\wedge\\
 	\bigwedge_{i\in RC}\bigvee_{j\in PC}\neg\Biggl(
 		& (c_ix-1>c_jx+c_jw\\
 		\nonumber & \vee c_ix+1+c_jw<c_jx\\
@@ -49,4 +49,54 @@ specified width and height.
 		\nonumber & \vee c_iy+1+c_jh<c_jh\Biggr)
 \end{align}
 
+All subformulas describe a constraint from the problem description and can be
+separated in three groups. Subformulas going over all components, only power
+components and only regular components.
+\begin{itemize}
+	\item\textbf{All}
+		\begin{enumerate}
+				\setcounter{enumi}{7}
+			\item Describes that the width and the height of the component can be
+				swapped(in case of rotation).
+			\item Constrains location of the components in regard to the size of
+				the chip.
+			\item Makes sure the components do not overlap by defining for all
+				pairs of components that they either are strictly right, strictly
+				left, strictly above or strictly below the other.
+		\end{enumerate}
+	\item\textbf{Power only}
+		\begin{enumerate}
+				\setcounter{enumi}{10}
+				\item Power components must be at least $17$ block away from
+					other power components. This is defined by saying that the
+					difference between the center of each pair of components is
+					bigger then $17$.
+		\end{enumerate}
+	\item\textbf{Regular only}
+		\begin{enumerate}
+				\setcounter{enumi}{11}
+				\item Regular components must be connected to a power
+						components. This is described using the method from the
+						overalap calculation in a negated way. Every regular
+						component must have overlap with a power component that
+						has been enlarged by $1$.
+		\end{enumerate}
+\end{itemize}
+
 \subsection{SMT format solution}
+The formula is easily convertable via a Python script to SMT format and said
+script is listed in Listing~\ref{listing:2.py}. The Python script optimizes a
+little bit from the original formula by leaving out the overlap checking
+between the same components. When we run the file a solution is found within
+$30$ seconds.
+
+\subsection{Solution}
+Figure~\ref{fig:s2} shows the configuration found by the solver. Light gray
+components are regular components and darker gray components are power
+components.
+
+\begin{figure}[H]
+	\includegraphics[scale=0.75]{s2.png}
+	\label{fig:s2}
+	\caption{Solution visualization for problem 2}
+\end{figure}
diff --git a/ar/assignments/Makefile b/ar/assignments/Makefile
index 2055aa8..4cfb119 100644
--- a/ar/assignments/Makefile
+++ b/ar/assignments/Makefile
@@ -1,4 +1,4 @@
-LATEX:=latex
+LATEX:=pdflatex
 
 DOCUMENT:=ar
 SOURCES:=$(filter-out preamble.tex,$(shell ls *.tex))
@@ -7,10 +7,7 @@ SOURCES:=$(filter-out preamble.tex,$(shell ls *.tex))
 
 all: $(DOCUMENT).pdf
 
-%.pdf: %.dvi
-	dvipdfm $<
-
-%.dvi: %.tex %.fmt $(SOURCES)
+%.pdf: %.tex %.fmt $(SOURCES)
 	$(LATEX) $(basename $@)
 	$(LATEX) $(basename $@)
 
diff --git a/ar/assignments/a.tex b/ar/assignments/a.tex
index 2c35ac5..8ac130a 100644
--- a/ar/assignments/a.tex
+++ b/ar/assignments/a.tex
@@ -1,6 +1,15 @@
 \section{Appendix}
+\begin{lstlisting}[caption={Benchmark system}]
+OS: Linux 3.16.0-4-amd64 #1 SMP Debian 3.16 x86_64 GNU/Linux
+CPU: 3600MHz AMD FX(tm)-4100 Quad-Core Processor
+RAM: 8GB
+\end{lstlisting}
+
 \newpage
 \lstinputlisting[language=lisp,caption={a1.smt},label={listing:a1.smt}]{src/1.smt}
 
+\newpage
+\lstinputlisting[language=python,caption={a2.py},label={listing:2.py}]{src/2.py}
+
 \newpage
 \lstinputlisting[language=python,caption={a4.py},label={listing:4.py}]{src/4.py}
diff --git a/ar/assignments/ar.tex b/ar/assignments/ar.tex
index fc99f80..94e25f9 100644
--- a/ar/assignments/ar.tex
+++ b/ar/assignments/ar.tex
@@ -1,11 +1,21 @@
 %&ar
 \begin{document}
 \maketitle
+\tableofcontents
 
+\newpage
 \input{1.tex}
+
+\newpage
 \input{2.tex}
+
+\newpage
 \input{3.tex}
+
+\newpage
 \input{4.tex}
+
+\newpage
 \input{a.tex}
 
 \end{document}
diff --git a/ar/assignments/preamble.tex b/ar/assignments/preamble.tex
index e9669d1..93b06ec 100644
--- a/ar/assignments/preamble.tex
+++ b/ar/assignments/preamble.tex
@@ -1,16 +1,17 @@
 \documentclass{article}
 
-\usepackage[dvipdfm]{hyperref}
+\usepackage{hyperref}
 \usepackage{a4wide}
 \usepackage{bm}
 \usepackage{float}
+\usepackage{graphicx}
 \usepackage{amsmath}
 \usepackage{listings}
 
 \everymath{\displaystyle}
 
 \lstset{%
-  basicstyle=\footnotesize,
+  basicstyle=\scriptsize,
   breakatwhitespace=true,
   breaklines=true,
   keepspaces=true,
diff --git a/ar/assignments/s2.png b/ar/assignments/s2.png
new file mode 100644
index 0000000..2876b39
Binary files /dev/null and b/ar/assignments/s2.png differ
diff --git a/ar/assignments/src/2.py b/ar/assignments/src/2.py
index 2b5ed99..e5852e6 100644
--- a/ar/assignments/src/2.py
+++ b/ar/assignments/src/2.py
@@ -1,5 +1,4 @@
 #!/usr/bin/env python3
-
 pc = [(4, 2), (4, 2), (4, 2)]
 rc = [(9, 7), (12, 6), (10, 7), (18, 5), (20, 4), (10, 6), (8, 6), (10, 8)]
 mx = 29
@@ -19,7 +18,6 @@ for i, (w, h) in enumerate(pc+rc, 1):
     print("(c{:02d}h Int)".format(i))
 print(")")
 
-# Preamble2
 print(":formula")
 print("(and")
 
@@ -27,67 +25,47 @@ print("(and")
 for i, (w, h) in enumerate(pc+rc, 1):
     # Print the width and height
     print((
-        '\t(or '
+        '(or '
         '(and (= c{0:02d}w {1}) (= c{0:02d}h {2})) '
-        '(and (= c{0:02d}w {2}) (= c{0:02d}h {1}))'
-        ')').format(i, w-1, h-1))
+        '(and (= c{0:02d}w {2}) (= c{0:02d}h {1})))').format(i, w-1, h-1))
 
-    # Print the bounds of the coordinates
+ # Print the bounds of the coordinates
     print((
-        '\t(> c{0:02d}x 0) (> c{0:02d}y 0)\n'
-        '\t(<= (+ c{0:02d}x c{0:02d}w) {1}) (<= (+ c{0:02d}y c{0:02d}h) {2})\n'
-        ).format(i, mx, my))
+         '(> c{0:02d}x 0) (> c{0:02d}y 0)'
+         '(<= (+ c{0:02d}x c{0:02d}w) {1}) (<= (+ c{0:02d}y c{0:02d}h) {2})'
+         ).format(i, mx, my))
 
-    # Print the non overlap with others
+ # Print the non overlap with others
     for j in range(1, 1+len(pc+rc)):
         if i != j:
             print((
-                '\t(or \n'
-                '\t\t(> c{0:02d}x (+ c{1:02d}x c{1:02d}w)) '
-                '(< (+ c{0:02d}x c{0:02d}w) c{1:02d}x)\n'
-                '\t\t(> c{0:02d}y (+ c{1:02d}y c{1:02d}h)) '
-                '(< (+ c{0:02d}y c{0:02d}h) c{1:02d}y)'
-                ')').format(i, j))
+                 '(or '
+                 '(> c{0:02d}x (+ c{1:02d}x c{1:02d}w)) (< (+ c{0:02d}x c{0:02d}w) c{1:02d}x) '
+                 '(> c{0:02d}y (+ c{1:02d}y c{1:02d}h)) (< (+ c{0:02d}y c{0:02d}h) c{1:02d}y)'
+                 ')').format(i, j))
 
-# Print the PC distance to eachother
+         # Print the PC distance to eachother
 for i, _ in enumerate(pc, 1):
     for j, _ in enumerate(pc, 1):
         if i != j:
             print((
-                '\t(or \n'
-                '\t\t(> \n'
-                '\t\t\t(- \n'
-                '\t\t\t\t(+ \n'
-                '\t\t\t\t\tc{0:02d}x \n'
-                '\t\t\t\t\t(/ c{0:02d}w 2) \n'
-                '\t\t\t\t) \n'
-                '\t\t\t\t(+ \n'
-                '\t\t\t\t\tc{1:02d}x \n'
-                '\t\t\t\t\t(/ c{1:02d}w 2) \n'
-                '\t\t\t\t) \n'
-                '\t\t\t) \n'
-                '\t\t\t{2} \n'
-                '\t\t)\n'
-                '\t\t(> (- (+ c{1:02d}x (/ c{1:02d}w 2)) '
-                '(+ c{0:02d}x (/ c{0:02d}w 2))) {2})\n'
-                '\t\t(> (- (+ c{0:02d}y (/ c{0:02d}h 2)) '
-                '(+ c{1:02d}y (/ c{1:02d}h 2))) {2})\n'
-                '\t\t(> (- (+ c{1:02d}y (/ c{1:02d}h 2)) '
-                '(+ c{0:02d}y (/ c{0:02d}h 2))) {2})'
+                '(or '
+                '(> (- (+ c{0:02d}x (/ c{0:02d}w 2) ) (+ c{1:02d}x (/ c{1:02d}w 2) ) ) {2} ) '
+                '(> (- (+ c{1:02d}x (/ c{1:02d}w 2)) (+ c{0:02d}x (/ c{0:02d}w 2))) {2}) '
+                '(> (- (+ c{0:02d}y (/ c{0:02d}h 2)) (+ c{1:02d}y (/ c{1:02d}h 2))) {2}) '
+                '(> (- (+ c{1:02d}y (/ c{1:02d}h 2)) (+ c{0:02d}y (/ c{0:02d}h 2))) {2})'
                 ')').format(i, j, pd))
 
-# Print the constraint that they have to be connected to a ps
+            # Print the constraint that they have to be connected to a ps
 for i, _ in enumerate(rc, 1+len(pc)):
-    print('\t(or')
+    print('(or')
     for j, _ in enumerate(pc, 1):
         print((
-            '\t(not (or \n'
-            '\t\t(> c{0:02d}x (+ c{1:02d}x 1 c{1:02d}w)) '
-            '(< (+ c{0:02d}x c{0:02d}w) (- c{1:02d}x 1))\n'
-            '\t\t(> c{0:02d}y (+ c{1:02d}y 1 c{1:02d}h)) '
-            '(< (+ c{0:02d}y c{0:02d}h) (- c{1:02d}y 1))'
+            '(not (or '
+            '(> c{0:02d}x (+ c{1:02d}x 1 c{1:02d}w)) (< (+ c{0:02d}x c{0:02d}w) (- c{1:02d}x 1)) '
+            '(> c{0:02d}y (+ c{1:02d}y 1 c{1:02d}h)) (< (+ c{0:02d}y c{0:02d}h) (- c{1:02d}y 1))'
             '))').format(i, j))
-    print('\t)')
+    print(')')
 
 # Close the and,benchmark parenthesis
 print("))")