diff options
Diffstat (limited to 'part1.tex')
-rw-r--r-- | part1.tex | 151 |
1 files changed, 132 insertions, 19 deletions
@@ -42,12 +42,13 @@ skipples. Nuzzles are very valuable: to distribute the risk of loss no two pallets of nuzzles may be in the same truck. -% (a) 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 eight trucks. -% and show how for that number all pallets may be divided over the eight trucks. - -% (b) Do the same, with the extra information that prittles and crottles are an explosive -% combination: they are not allowed to be put in the same truck. +\begin{itemize} +\item[(a)] 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 eight trucks. +\item[(b)] Do the same, with the extra information that prittles and crottles +are an explosive combination: they are not allowed to be put in the same truck. +\end{itemize} \subsection*{Solution:} \subsubsection*{(a)} @@ -239,13 +240,13 @@ then we have to check pairs that we have not seen yet: \bigwedge_{0 \leq i < m} \bigwedge_{i < j < m} cx_i \geq& cx_j + powerDistance \lor -cx_j \geq cx_i + powerDistance \lor \\ +cx_j \geq cx_i + powerDistance \lor \nonumber \\ cy_i \geq& cy_j + powerDistance \lor cy_j \geq cy_i + powerDistance \end{align} 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}, +(ingredients \ref{eq:chip1}, \ref{eq:chip2}, \ref{eq:chip3}, \ref{eq:chip4} and \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. @@ -339,12 +340,13 @@ Twelve jobs numbered from 1 to 12 have to be executed satisfying the following r no two of these jobs may run at the same time. \end{itemize} -% (a) Find a solution of this scheduling problem for which the total running time is -% minimal. - -% (b) Do the same with the extra requirement that job 6 and job 12 need a resource of -% limited availability, by which job 6 may only run during the 17 time units in which -% job 12 is running. +\begin{itemize} +\item[(a)] Find a solution of this scheduling problem for which the total + running time is minimal. +\item[(b)] Do the same with the extra requirement that job 6 and job 12 need a + resource of limited availability, by which job 6 may only run during the 17 + time units in which job 12 is running. +\end{itemize} \subsection*{Solution:} \subsubsection*{(a)} @@ -423,16 +425,127 @@ are given, for which the initial value of $a_i$ is $i$ for $i = 1$, \ldots, 8. The following steps are defined: choose $i$ with $1 < i < 8$ and execute \[ - a_i := a_{i-1} + a_i+1, + a_i := a_{i-1} + a_{i+1}, \] that is, $a_i$ gets the sum of the values of its neighbors and all other values remain unchanged. -% (a) Show how it is possible that $a_3 = a_7$ after a number of steps. - -% (b) Show how it is possible that $a_3 = a_5 = a_7$ after a number of steps. -% For this problem both try to use an SMT solver and NuSMV, and discuss how they perform. +\begin{itemize} +\item[(a)] Show how it is possible that $a_3 = a_7$ after a number of steps. +\item[(b)] Show how it is possible that $a_3 = a_5 = a_7$ after a number of steps. +For this problem both try to use an SMT solver and NuSMV, and discuss how they perform. +\end{itemize} \subsection*{Solution:} +\subsubsection*{(a)} +We generalize this problem to $n$ variables $a_1, a_2, \ldots, a_n$. Let +$a_{i,0}$ denote the variables $a_i$ in the initial state. +Let $m$ denote the number of steps we need to reach the desired configuration +(this is the value we have to find out). +Let $a_{i,s}$ denote the variables $a_i$ after $1 \leq s \leq m$ steps. + +A sketch of the solution will involve $n \times (1 + m)$ literals ($n$ in the +initial state, $n \times m$ after $m$ steps). The formula will consist of a +conjunction of the initial states, transition relations and an ingredient +describing the desired configuration. + +(Note that the given change ($a_{i,s} = a_{i-1,s-1} + a_{i+1,s-1}$ for $1 < i < +n$ and $1 \leq s \leq m$) will always keep the first and last values unchanged +throughout the execution. So only one $a_1$ and $a_n$ would be sufficient. For +symmetry with all other variables, and to allow for arbitrary other changes in a +step, we have decided to keep this though.) + +The ingredient to model the initial state: +\begin{align} +\label{eq:sum1} +\bigwedge_{i=1}^n a_{i,0} = i +\end{align} + +Next, we try to reach the goal of finding $a_3=a_7$ in any state: +\begin{align} +\label{eq:sum2} +\bigvee_{s=0}^m a_{3,s} = a_{7,s} +\end{align} +Technically we can start with $s=1$ instead of $s=0$ since the values in the +initial state are all unique. We chose to keep it though such that the solution +can be generalized for arbitrary values in the initial state. + +Finally we add the transition relations for each step $1 \leq s \leq m$ (reached +from the previous step $s-1$). In each transition, one variable $1 < i < n$ will +be changed to match the (previous) values of the neighbors while all others are +unchanged from the previous state: +\begin{align} +\label{eq:sum3} +\bigwedge_{s=1}^m +\bigvee_{i=2}^{n-1} ( +a_{i,s} = a_{i-1,s-1} + a_{i+1,s-1} \land +\bigwedge_{1 \leq j \leq n, i \neq j} a_{j,s} = a_{j,s-1} +) +\end{align} + +The conjunction of ingredients \ref{eq:sum1}, \ref{eq:sum2} and \ref{eq:sum3} +form the formula that is parameterized by $n$ and $m$. For our problem, $n=8$ so +we have to find $m$. At first we picked $m=20$ (arbitrary) and then narrowed +down $m$ using a binary search. In the end we found that $m=7$ is the minimum +solution. The resulting assignment was obtained using the command +\texttt{python generate-neighborsum.py 7 | z3 -smt -in} and is summarized in +Table~\ref{tbl:sumA}. The annotated, generated input for \texttt{z3} is shown in +Listing~\ref{lst:sumA}. + +\begin{table}[H] +\centering +\begin{tabular}{r|rrrrrrrr} + & $a_1$ & $a_2$ & $a_3$ & $a_4$ & $a_5$ & $a_6$ & $a_7$ & $a_8$ \\ +\hline + 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 \\ + 1 & 1 & 2 & \bf 6 & 4 & 5 & 6 & 7 & 8 \\ + 2 & 1 & 2 & 6 & \bf11 & 5 & 6 & 7 & 8 \\ + 3 & 1 & 2 & \bf13 & 11 & 5 & 6 & 7 & 8 \\ + 4 & 1 & 2 & 13 & \bf18 & 5 & 6 & 7 & 8 \\ + 5 & 1 & 2 & 13 & 18 & 5 & \bf12 & 7 & 8 \\ + 6 & 1 & 2 & 13 & 18 & 5 & 12 & \bf20 & 8 \\ + 7 & 1 & 2 & \bf20 & 18 & 5 & 12 & 20 & 8 \\ +\end{tabular} +\caption{\label{tbl:sumA}The values of each variable where the modified values +in each step are highlighted.} +\end{table} + +\begin{lstlisting}[ + caption={Generated SMT output for $n=8, m=7$ that satisfies $a_3=a_7$}, + label={lst:sumA},language=lisp,basicstyle=\scriptsize +] +(benchmark test.smt +:logic QF_UFLIA +:extrafuns ( +(a1_0 Int) ... (a8_0 Int) +... +(a1_7 Int) ... (a8_7 Int) +) +:formula (and +(= a1_0 1) ... (= a8_0 8) +; trying to reach the goal in each state +(or (= a3_0 a7_0) ... (= a3_7 a7_7)) +; in each state, one of the n-2=6 values must change, +; while leaving the others unchanged from the previous state. +(or + (and (= a2_1 (+ a1_0 a3_0)) + (= a1_1 a1_0) ... (= a8_1 a8_0)) + ... + (and (= a7_1 (+ a6_0 a8_0)) + (= a1_1 a1_0) ... (= a8_1 a8_0)) +) +... +(or + (and (= a2_7 (+ a1_6 a3_6)) + (= a1_7 a1_6) ... (= a8_7 a8_6)) + ... + (and (= a7_7 (+ a6_6 a8_6)) + (= a1_7 a1_6) ... (= a8_7 a8_6)) + ) +)) + +\end{lstlisting} + +\subsubsection*{(b)} \end{document} |