From: Mart Lubbers Date: Thu, 8 Oct 2015 17:16:58 +0000 (+0200) Subject: a14 af X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=d6e52075a46bb2c6ac69964655d10292ff144450;p=master.git a14 af --- diff --git a/ar/assignments/1.tex b/ar/assignments/1.tex index 56b444d..a49218a 100644 --- a/ar/assignments/1.tex +++ b/ar/assignments/1.tex @@ -1,5 +1,4 @@ -\paragraph{Problem 1} - +\section{Problem 1} {\em Six trucks have to deliver pallets of obscure building blocks to a magic factory. Every ruck has a capacity of 7800 kg and can carry at most diff --git a/ar/assignments/4.tex b/ar/assignments/4.tex index e0f3ac0..64c65c7 100644 --- a/ar/assignments/4.tex +++ b/ar/assignments/4.tex @@ -1,9 +1,7 @@ -\paragraph{Problem 4} - +\section{Problem 4} {\em Seven integer variables $a_1; a_2; a_3; a_4; a_5; a_6; a_7$ are given, for -which the initial value of $a_i$ is $i$ for $i=1,\ldots,7$. The following steps -are defined: choose $i$ with $1= 50\right)\wedge\left( - \bigvee_{j=2}^{I-1}\left(i_Na_k=i_Na_j\right)\wedge - \left(k\neq j\right) +\subsection{Formal definition} +\paragraph{Precondition} +Say we have $I$ $a$'s denoted as $a_i$ and we have $N$ iterations. $i_na_i$ +means variable $a_i$ in iteration $n$. Iteration $0$ is seen as the starting +point and can be expressed as in Equation~\ref{eq:4pre} + +\begin{equation}\label{eq:4pre} + (a_1=1)\wedge + (a_I=I)\wedge + \bigwedge_{k=2}^{I-1} (i_0a_i=i)\\ +\end{equation} + +\paragraph{Program} +Every iteration we can choose to do $a_i=a_{i-1}+a_{i+1}$ or nothing. To keep +track of what we do we keep a counter $c_n$ for every $n$ that holds either the +$i$ if an $a_i$ is chosen or $0$ if no action has been taken. Therefore for all +iterations we can express this as in Equation~\ref{eq:4pro} + +{\medmuskip=0mu \thinmuskip=0mu \thickmuskip=0mu +\begin{equation} +\label{eq:4pro} + \bigwedge_{n=1}^{N}\left( + \bigvee_{k=2}^{I-1}\left( + (c_i = k) + \wedge + (i_na_j = i_{n-1}a_{j-1} + i_{n-1}a_{j+1}) + \wedge + \bigwedge_{j=2}^{I-1}\left( + (j\neq k)\wedge (i_na_j = i_{n-1}a_j) + \right) + \right) + \vee + \bigwedge_{k=2}^{I-1}(i_na_k = i_{n-1}a_k) \wedge (c_i=0) \right) -\right)$$ +\end{equation} +} + +\paragraph{Postcondition} +Finally the post condition can be described as $a_i>50$ and some other +$a_i= a_j\wedge i\neq j$ for all $i$. This is expressed in +Equation~\ref{eq:4pst} + +\begin{equation}\label{eq:4pst} + \bigvee_{k=2}^{I-1}\left( + (i_Na_k >= 50)\wedge + \left(\bigvee_{j=2}^{I-1}(i_Na_k=i_Na_j)\wedge(k\neq j)\right) + \right) +\end{equation} + +\paragraph{Total} +To tie this all together we just put $\wedge$ in between and that results in: +$$\text{precondition }\wedge\text{ program }\wedge\text{ postcondition}$$ + +\subsection{SMT format solution} +Naming the precondition, program and postcondition respectively $p_1, p_2, p_3$ +we can easily convert it to a SMT format. The converting is tedious and takes a +lot of time and therefore an automatization script has been created that is +visible in the appendices in Listing~\ref{listing:4.py}. The script +automatically assumes $11$ iterations and $7$ $a_i$ variables but via command +line arguments this is easily extendable. To determine the minimal number of +iterations a simple bash script can be made that iteratively increases the +iterations as shown in Listing~\ref{listing:4bash}. The shortest solution with +length $11$ is found in around $30$ seconds. Finding the smallest solution +length incrementally takes around $75$ seconds. + +\begin{lstlisting}[language=bash, + caption={Iteratively find the shortest solution},label={listing:4bash}] +i=1 +while [ "$(python a4.py $i | yices-smt)" = "unsat" ] +do + i=$((i+1)) + echo $i; +done +\end{lstlisting} +\subsection{Solution} +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 @@ -50,5 +102,6 @@ $\begin{array}{c|c|ccccc} 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}\\ + 10 & 6 & 4 & 54 & 50 & 47 & \bm{54} \end{array}$ +\end{center} diff --git a/ar/assignments/a.tex b/ar/assignments/a.tex new file mode 100644 index 0000000..cc957af --- /dev/null +++ b/ar/assignments/a.tex @@ -0,0 +1,3 @@ +\section{Appendix} +\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 a85b3f2..fc99f80 100644 --- a/ar/assignments/ar.tex +++ b/ar/assignments/ar.tex @@ -6,5 +6,6 @@ \input{2.tex} \input{3.tex} \input{4.tex} +\input{a.tex} \end{document} diff --git a/ar/assignments/preamble.tex b/ar/assignments/preamble.tex index 477b06f..7fde354 100644 --- a/ar/assignments/preamble.tex +++ b/ar/assignments/preamble.tex @@ -2,9 +2,25 @@ \usepackage{a4wide} \usepackage{bm} +\usepackage{amsmath} +\usepackage{listings} \everymath{\displaystyle} +\lstset{% + basicstyle=\footnotesize, + breakatwhitespace=true, + breaklines=true, + keepspaces=true, + numbers=left, + numberstyle=\tiny, + frame=L, + showspaces=false, + showstringspaces=false, + showtabs=false, + tabsize=2 +} + \author{Mart Lubbers (s4109503)} \title{Automated reasoning Assignment 1} \date{\today} diff --git a/ar/assignments/src/4.py b/ar/assignments/src/4.py index e260264..51d5347 100644 --- a/ar/assignments/src/4.py +++ b/ar/assignments/src/4.py @@ -1,5 +1,7 @@ -iterations = 11 -numa = 8 +#!/usr/bin/env python3 +import sys +iterations = int(sys.argv[1]) if len(sys.argv) > 1 else 11 +numa = int(sys.argv[2]) if len(sys.argv) > 2 else 7 ##Print preamble print("(benchmark a4.smt") @@ -52,8 +54,7 @@ for v in range(2, numa): for ov in [k for k in range(2, numa) if k != v]: print("(= i{0}a{1} i{0}a{2})".format(iterations-1, v, ov)) print("))") - - print(")") + ## Close the and,benchmark parenthesis print("))")