From: Mart Lubbers Date: Mon, 19 Oct 2015 18:24:22 +0000 (+0200) Subject: update finished a1 X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=235422a1ebe3aec633751a0006ecd0a9af7ac516;p=master.git update finished a1 --- diff --git a/ar/assignments/1.tex b/ar/assignments/1.tex index a49218a..f45e8b4 100644 --- a/ar/assignments/1.tex +++ b/ar/assignments/1.tex @@ -1,7 +1,7 @@ \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 +factory. Every truck has a capacity of 7800 kg and can carry at most eight pallets. In total, the following has to be delivered:\\ \begin{itemize} \item Four pallets of nuzzles, each of weight 700 kg. @@ -20,4 +20,73 @@ delivered, and show how for that number all pallets may be divided over the six trucks. } +\subsection{Formal definition} +For every truck $t_i$ for $i\in[1\ldots6]$ in combination with every nuzzle +$n$, prittle $p$, skipple $s$, crottle $c$ and dupple $d$ we declare a variable +that holds the amount of that type of building block. For truck 1 we thus have +the variables: $t_1n, t_1p, t_1s, t_1c, t_1d$. +To lay a contraint on the weight we declare for every truck the following rule. +$$\bigwedge^{T}_{i=1}\left(t_in*700+t_ip*800+t_is*1000+t_ic*1500+t_id*100<7800\right)$$ + +To limit the maximum number of pallets in a truck we define. +$$\bigwedge^{T}_{i=1}\left(\left(\sum_{p\in\{n,p,s,c,d\}}t_ip\right)\leq8\right)$$ + +To limit the minimum number of pallets in a truck we define. +$$\bigwedge^{T}_{i=1}\bigwedge_{p\in\{n,p,s,c,d\}}t_ip>0$$ + +To describe the number of pallets available we define for every type of pallet +a variable that describes the number available if there is a limited number +available. +$$num_n=4\wedge num_s=8\wedge num_c=10\wedge num_d=5$$ + +To be sure the materials are all delivered we define. +$$\bigwedge_{p\in\{n,s,c,d\}}\left(\left(\sum^{T}_{i=1}t_ip\right)=num_p\right)$$ + +The first constraint is that prittles and crottles can not be in the same +truck. This is easily described with. +$$\bigwedge^{T}_{i=1}\left(t_ip=0\vee t_ic=0\right)$$ + +Skipples need to be cooled and only two trucks have cooling. Therefore we +specify. +$$\bigwedge^{T}_{i=3}t_is=0$$ + +Dupples can only be in a truck with a maximum of two. +$$\bigwedge^{T}_{i=1}t_id\leq1$$ + +We can tie this together by putting $\wedge$ symbols between all of the +formulas. + +\subsection{SMT format solution} +The formula is easily convertable to SMT format and is listed in +Listing~\ref{listing:a1.smt}. A final condition is added with a special +variable named \texttt{} that we increment to find the maximum amount of +prittles transportable. When running the script in Listing~\ref{listing:1bash} +the loop terminates after it echoed $20$ meaning that the maximum number of +prittles is 20. This iterative solution takes less then $0.1$ seconds to +calculate. + +\begin{lstlisting}[language=bash, + caption={Iteratively find the largest solution},label={listing:1bash}] +i=1 +while [ $(sed "s//$i/g" a1.smt | yices-smt) = "sat" ] +do + echo $((++i)); +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} diff --git a/ar/assignments/4.tex b/ar/assignments/4.tex index 64c65c7..b74707d 100644 --- a/ar/assignments/4.tex +++ b/ar/assignments/4.tex @@ -79,8 +79,7 @@ length incrementally takes around $75$ seconds. i=1 while [ "$(python a4.py $i | yices-smt)" = "unsat" ] do - i=$((i+1)) - echo $i; + echo $((++i)); done \end{lstlisting} diff --git a/ar/assignments/a.tex b/ar/assignments/a.tex index cc957af..b676ffe 100644 --- a/ar/assignments/a.tex +++ b/ar/assignments/a.tex @@ -1,3 +1,6 @@ \section{Appendix} +\newpage +\lstinputlisting[language=lisp,caption={a1.smt},label={listing:a1.smt}]{src/a1.smt} + \newpage \lstinputlisting[language=python,caption={a4.py},label={listing:4.py}]{src/4.py} diff --git a/ar/assignments/src/a1.smt b/ar/assignments/src/a1.smt index 2bfa67e..77871e1 100644 --- a/ar/assignments/src/a1.smt +++ b/ar/assignments/src/a1.smt @@ -1,19 +1,60 @@ (benchmark a1.smt :logic QF_UFLIA :extrafuns ( - (MaxTruck Int) - (NuzzleWeight Int) - (PrittleWeight Int) - (SkippleWeight Int) - (CrottleWeight Int) - (DuppleWeight Int) + (t1p Int) (t1n Int) (t1s Int) (t1c Int) (t1d Int) + (t2p Int) (t2n Int) (t2s Int) (t2c Int) (t2d Int) + (t3p Int) (t3n Int) (t3s Int) (t3c Int) (t3d Int) + (t4p Int) (t4n Int) (t4s Int) (t4c Int) (t4d Int) + (t5p Int) (t5n Int) (t5s Int) (t5c Int) (t5d Int) + (t6p Int) (t6n Int) (t6s Int) (t6c Int) (t6d Int) ) :formula (and - (= NuzzleWeight 700) - (= PrittleWeight 800) - (= SkippleWeight 1000) - (= CrottleWeight 1500) - (= DuppleWeight 100) + (>= t1p 0) (>= t1n 0) (>= t1s 0) (>= t1c 0) (>= t1d 0) + (>= t2p 0) (>= t2n 0) (>= t2s 0) (>= t2c 0) (>= t2d 0) + (>= t3p 0) (>= t3n 0) (>= t3s 0) (>= t3c 0) (>= t3d 0) + (>= t4p 0) (>= t4n 0) (>= t4s 0) (>= t4c 0) (>= t4d 0) + (>= t5p 0) (>= t5n 0) (>= t5s 0) (>= t5c 0) (>= t5d 0) + (>= t6p 0) (>= t6n 0) (>= t6s 0) (>= t6c 0) (>= t6d 0) + + (<= (+ t1p t1n t1s t1c t1d) 8) + (<= (+ t2p t2n t2s t2c t2d) 8) + (<= (+ t3p t3n t3s t3c t3d) 8) + (<= (+ t4p t4n t4s t4c t4d) 8) + (<= (+ t5p t5n t5s t5c t5d) 8) + (<= (+ t6p t6n t6s t6c t6d) 8) + + (<= (+ (* t1n 700) (* t1p 800) (* t1s 1000) (* t1c 1500) (* t1d 100)) 7800) + (<= (+ (* t2n 700) (* t2p 800) (* t2s 1000) (* t2c 1500) (* t2d 100)) 7800) + (<= (+ (* t3n 700) (* t3p 800) (* t3s 1000) (* t3c 1500) (* t3d 100)) 7800) + (<= (+ (* t4n 700) (* t4p 800) (* t4s 1000) (* t4c 1500) (* t4d 100)) 7800) + (<= (+ (* t5n 700) (* t5p 800) (* t5s 1000) (* t5c 1500) (* t5d 100)) 7800) + (<= (+ (* t6n 700) (* t6p 800) (* t6s 1000) (* t6c 1600) (* t6d 100)) 7800) + + (= (+ t1n t2n t3n t4n t5n t6n) 4) + (= (+ t1s t2s t3s t4s t5s t6s) 8) + (= (+ t1c t2c t3c t4c t5c t6c) 10) + (= (+ t1d t2d t3d t4d t5d t6d) 5) + + (or (= 0 t1p) (= 0 t1c)) + (or (= 0 t2p) (= 0 t2c)) + (or (= 0 t3p) (= 0 t3c)) + (or (= 0 t4p) (= 0 t4c)) + (or (= 0 t5p) (= 0 t5c)) + (or (= 0 t6p) (= 0 t6c)) + + (= t3s 0) + (= t4s 0) + (= t5s 0) + (= t6s 0) + + (<= t1d 1) + (<= t2d 1) + (<= t3d 1) + (<= t4d 1) + (<= t5d 1) + (<= t6d 1) + + (>= (+ t1p t2p t3p t4p t5p t6p) ) ) )