{\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.
\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
\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}
+\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}
\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}
\documentclass{article}
+\usepackage[dvipdfm]{hyperref}
\usepackage{a4wide}
\usepackage{bm}
+\usepackage{float}
\usepackage{amsmath}
\usepackage{listings}
--- /dev/null
+#!/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("))")
repositories / master.git / commitdiff