From a01304944e3aafcfa4cc17275a1854de08dd29e1 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Tue, 20 Oct 2015 13:49:18 +0200 Subject: [PATCH] update --- ar/assignments/1.tex | 46 ++++++++++++++---------- ar/assignments/2.tex | 51 ++++++++++++++++++++++++++ ar/assignments/4.tex | 39 +++++++++++--------- ar/assignments/preamble.tex | 2 ++ ar/assignments/src/2.py | 72 +++++++++++++++++++++++++++++++++++++ 5 files changed, 175 insertions(+), 35 deletions(-) create mode 100644 ar/assignments/src/2.py diff --git a/ar/assignments/1.tex b/ar/assignments/1.tex index 51fc39e..317ae58 100644 --- a/ar/assignments/1.tex +++ b/ar/assignments/1.tex @@ -2,7 +2,7 @@ {\em Six trucks have to deliver pallets of obscure building blocks to a magic factory. Every truck has a capacity of 7800 kg and can carry at most -eight pallets. In total, the following has to be delivered:\\ +eight pallets. In total, the following has to be delivered: \begin{itemize} \item Four pallets of nuzzles, each of weight 700 kg. \item A number of pallets of prittles, each of weight 800 kg. @@ -11,15 +11,17 @@ eight pallets. In total, the following has to be delivered:\\ \item Five pallets of dupples, each of weight 100 kg. \end{itemize} Prittles and crottles are an explosive combination: they are not allowed to be -put in the same truck.\\ +put in the same truck. + Skipples need to be cooled; only two of the six trucks have facility for cooling skipples. Dupples are very valuable; to distribute the risk of loss no -two pallets of dupples may be in the same truck.\\ +two pallets of dupples may be in the same truck. + Investigate what is the maximum number of pallets of prittles that can be delivered, and show how for that number all pallets may be divided over the six trucks. } -\newpage + \subsection{Formal definition} For every truck $t_i$ for $i\in T$ where $T=[1\ldots6]$ in combination with every nuzzle $n$, prittle $p$, skipple $s$, crottle $c$ and dupple $d$ we @@ -94,17 +96,25 @@ done \end{lstlisting} \subsection{Solution} -\begin{tabular}{|l|lllll|l|l|} - \hline - Truck & Nuzzles & Prittles & Skipples & Crottles & Dupples & Weight & Pallets\\ - \hline - 1 & 0 & 0 & 4 & 2 & 1 & 7100 & 7\\ - 2 & 0 & 3 & 4 & 0 & 1 & 6500 & 8\\ - 3 & 0 & 8 & 0 & 0 & 0 & 6400 & 7\\ - 4 & 0 & 7 & 0 & 0 & 1 & 5700 & 8\\ - 5 & 0 & 0 & 0 & 5 & 1 & 7600 & 6\\ - 6 & 4 & 0 & 0 & 3 & 1 & 7400 & 8\\ - \hline - total & 4 & 18 & 8 & 10 & 5 & &\\ - \hline -\end{tabular} +The iterative solution terminates with $i=18$ so the maximum number of prittles +to be deliverd is $18$. When we rerun the solution with $18$ prittles and the +\texttt{-m} flag we can see the solution as in Table~\ref{tab:s1}. + +\begin{table}[H] + \begin{tabular}{|l|lllll|l|l|} + \hline + Truck & Nuzzles & Prittles & Skipples & Crottles & Dupples & Weight & Pallets\\ + \hline + 1 & 0 & 0 & 4 & 2 & 1 & 7100 & 7\\ + 2 & 0 & 3 & 4 & 0 & 1 & 6500 & 8\\ + 3 & 0 & 8 & 0 & 0 & 0 & 6400 & 7\\ + 4 & 0 & 7 & 0 & 0 & 1 & 5700 & 8\\ + 5 & 0 & 0 & 0 & 5 & 1 & 7600 & 6\\ + 6 & 4 & 0 & 0 & 3 & 1 & 7400 & 8\\ + \hline + total & 4 & 18 & 8 & 10 & 5 & &\\ + \hline + \end{tabular} + \caption{Solution table for problem 1} + \label{tab:s1} +\end{table} diff --git a/ar/assignments/2.tex b/ar/assignments/2.tex index e69de29..d1b13f1 100644 --- 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_jwc_jy+c_jh\\ + \nonumber & \qquad\qquad\qquad \vee c_iy+c_jh15\\ + \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} diff --git a/ar/assignments/4.tex b/ar/assignments/4.tex index b74707d..dd52191 100644 --- a/ar/assignments/4.tex +++ b/ar/assignments/4.tex @@ -84,23 +84,28 @@ done \end{lstlisting} \subsection{Solution} +The iterative solution terminates with $i=11$ so the minimum number of steps +required is $11$. When we rerun the solution with $11$ steps and the +\texttt{-m} flag we can see the solution as in Table~\ref{tab:s4}. The bold cells represent the $a_i$ after applying the function. After ten iterations cell $a_2$ and $a_6$ both hold $54$ thus satisfying the problem specification. -\begin{center} -$\begin{array}{c|c|ccccc} - \# & i & a_2 & a_3 & a_4 & a_5 & a_6\\ - \hline - 0 & - & 2 & 3 & 4 & 5 & 6\\ - 1 & 4 & 2 & 3 & \bm{8} & 5 & 6\\ - 2 & 5 & 2 & 3 & 8 & \bm{14} & 6\\ - 3 & 2 & \bm{4} & 3 & 8 & 14 & 6\\ - 4 & 4 & 4 & 3 & \bm{17} & 14 & 6\\ - 5 & 5 & 4 & 3 & 17 & \bm{23} & 6\\ - 6 & 6 & 4 & 3 & 17 & 23 & \bm{30}\\ - 7 & 5 & 4 & 3 & 17 & \bm{47} & 30\\ - 8 & 4 & 4 & 3 & \bm{50} & 47 & 30\\ - 9 & 3 & 4 & \bm{54} & 50 & 47 & 30\\ - 10 & 6 & 4 & 54 & 50 & 47 & \bm{54} -\end{array}$ -\end{center} +\begin{table}[H] + \begin{tabular}{c|c|ccccc} + \# & $i$ & $a_2$ & $a_3$ & $a_4$ & $a_5$ & $a_6$\\ + \hline + $0$ & - & $2$ & $3$ & $4$ & $5$ & $6$\\ + $1$ & $4$ & $2$ & $3$ & $\bm{8}$ & $5$ & $6$\\ + $2$ & $5$ & $2$ & $3$ & $8$ & $\bm{14}$ & $6$\\ + $3$ & $2$ & $\bm{4}$ & $3$ & $8$ & $14$ & $6$\\ + $4$ & $4$ & $4$ & $3$ & $\bm{17}$ & $14$ & $6$\\ + $5$ & $5$ & $4$ & $3$ & $17$ & $\bm{23}$ & $6$\\ + $6$ & $6$ & $4$ & $3$ & $17$ & $23$ & $\bm{30}$\\ + $7$ & $5$ & $4$ & $3$ & $17$ & $\bm{47}$ & $30$\\ + $8$ & $4$ & $4$ & $3$ & $\bm{50}$ & $47$ & $30$\\ + $9$ & $3$ & $4$ & $\bm{54}$ & $50$ & $47$ & $30$\\ + $10$ & $6$ & $4$ & $54$ & $50$ & $47$ & $\bm{54}$ + \end{tabular} +\caption{Solution table for problem 4} +\label{tab:s4} +\end{table} diff --git a/ar/assignments/preamble.tex b/ar/assignments/preamble.tex index 7fde354..e9669d1 100644 --- a/ar/assignments/preamble.tex +++ b/ar/assignments/preamble.tex @@ -1,7 +1,9 @@ \documentclass{article} +\usepackage[dvipdfm]{hyperref} \usepackage{a4wide} \usepackage{bm} +\usepackage{float} \usepackage{amsmath} \usepackage{listings} diff --git a/ar/assignments/src/2.py b/ar/assignments/src/2.py new file mode 100644 index 0000000..f276fcb --- /dev/null +++ b/ar/assignments/src/2.py @@ -0,0 +1,72 @@ +#!/usr/bin/env python3 + +pc = [(4, 22), (4, 22), (4, 22)] +rc = [(9, 7), (12, 6), (10, 7), (18, 5), (20, 4), (10, 6), (8, 6), (10, 8)] + +##Print preamble +print("(benchmark a4.smt") +print(":logic QF_UFLIA") + +##Print variables +print(":extrafuns (") +for i, (w, h) in enumerate(pc+rc, 1): + print("(c{:02d}x Int)".format(i), end=' ') + print("(c{:02d}y Int)".format(i), end=' ') + print("(c{:02d}w Int)".format(i), end=' ') + print("(c{:02d}h Int)".format(i), end=' ') +print(")") + +##Preamble2 +print(":formula") +print("(and") + +##Print the PC and RC subformulas +for i, (w, h) in enumerate(pc+rc, 1): + ##Print the width and height + print(( + '\t(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, h)) + + ##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) 29) (<= (+ c{0:02d}y c{0:02d}h) 22)\n' + ).format(i, w, h)) + + ##Print the non overlap with others + for j in range(1, 1+len(pc+rc)): + print(( + '\t(or (= {0} {1})\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)) + +##Print the PC distance to eachother +for i, _ in enumerate(pc, 1): + for j, _ in enumerate(pc, 1): + print(( + '\t(or (= {0} {1})\n' + '\t\t(> (- (/ (+ c{0:02d}x c{0:02d}w) 2) (/ (+ c{1:02d}x c{1:02d}w) 2)) 17)\n' + '\t\t(> (- (/ (+ c{1:02d}x c{1:02d}w) 2) (/ (+ c{0:02d}x c{0:02d}w) 2)) 17)\n' + '\t\t(> (- (/ (+ c{0:02d}y c{0:02d}h) 2) (/ (+ c{1:02d}y c{1:02d}h) 2)) 17)\n' + '\t\t(> (- (/ (+ c{1:02d}y c{1:02d}h) 2) (/ (+ c{0:02d}y c{0:02d}h) 2)) 17)' + ')').format(i, j)) + +#Print the constraint that they have to be connected to a ps +for i, _ in enumerate(rc, 1+len(pc)): + print('\t(or') + for j, _ in enumerate(pc, 1): + print(( + '\t\t(= c{0:02d}x (+ c{1:02d}x c{1:02d}w 1))\n' + '\t\t(= (+ c{0:02d}x c{0:02d}w 1) c{1:02d}x)\n' + '\t\t(= c{0:02d}y (+ c{1:02d}y c{1:02d}h 1))\n' + '\t\t(= (+ c{0:02d}y c{0:02d}h 1) c{1:02d}y)' + ).format(i, j)) + print('\t)') + +## Close the and,benchmark parenthesis +print("))") -- 2.20.1