From: Mart Lubbers Date: Thu, 22 Oct 2015 19:31:25 +0000 (+0200) Subject: finished 1-3 X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=0ceec1deebde03d3e5c4d2081c5d54ce2fddd01b;p=master.git finished 1-3 --- diff --git a/ar/assignments/1.tex b/ar/assignments/1.tex index 317ae58..8506da9 100644 --- a/ar/assignments/1.tex +++ b/ar/assignments/1.tex @@ -22,46 +22,48 @@ 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 +For every truck $t_i$ for $i\in T$ where $T=\{1,\ldots,6\}$ 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. -We group all pallets $r$ for $r\in P$ where $P=[n,p,s,c,d]$. We also define -function $w(r)$ that defines the weight of the pallet and $n(r)$ that defines -the number of pallets needed. Then the following combination of subformulas -describes the problem. +declare a variable that holds the amount of that type of building block in that +truck. We group all pallets $r\in P$ where $P=\{n,p,s,c,d\}$. We also +define function $w(r)$ that defines the weight of the pallet and $n(r)$ that +defines the number of pallets needed. + +This leads to the following formalization where we maximize $n(p)$. \begin{align} \bigwedge^{T}_{i=1}\Biggl( - & \bigwedge_{r\in P}t_ir\geq0\\ - & \wedge \sum_{r\in P}t_ir\leq8\\ - & \wedge \left(\sum_{r\in P}t_ir*w(r)\right)\leq7800)\\ - & \wedge (t_ip=0\vee t_ic=0)\\ - & \wedge t_id\leq1\\ - & \wedge (t_i=t_1 \vee t_i=t_2 \vee t_is=0)\Biggr)\wedge\\ + & \bigwedge_{r\in P}t_{i}r\geq0\\ + & \wedge \sum_{r\in P}t_{i}r\leq8\\ + & \wedge \left(\sum_{r\in P}t_{i}r\cdot w(r)\right)\leq7800)\\ + & \wedge (t_{i}p=0\vee t_{i}c=0)\\ + & \wedge t_{i}d\leq1\\ + & \wedge (t_{i}=t_{1} \vee t_{i}=t_{2} \vee t_{i}s=0)\Biggr)\wedge\\ \bigwedge_{r\in P}\Biggl( - & r=p\vee\left(\sum^{T}_{i=1}t_ir\right)=n(r)\Biggr) + & \left(\sum^{T}_{i=1}t_{i}r\right)=n(r)\Biggr) \end{align} -All the subformulas describe a constraint from the problem description and we -can separate two groups. Subformulas going over all trucks and subformulas over -all pallets. +Every numbered subformula describes a constraint from the problem description. +We can separated the subformulas in formulas going over all trucks and formulas +going over all pallets. + \begin{itemize} \item \textbf{Trucks} \begin{enumerate} - \item Makes sure you can not have a negative number of pallets. - by stating that all pallets numbers per truck are - bigger then $0$. + \item Makes sure you can not have a negative number of pallets + in a truck by stating that the number of pallets in a + truck is not smaller then $0$. \item Makes sure you can not have more then $8$ pallets in a truck by stating that the sum of all pallets in a truck is not bigger then $8$. - \item Makes sure the weight will never go over the maximum by - stating that all the pallets times their weight in a - truck may not go over $7800$kg. + \item Makes sure the weight will never go over the maximum + weight per truck by stating that all the pallets times + their weight in a truck will not go over $7800$kg. \item Makes sure prittles and crottles are never together in a truck by stating that either the number of prittles is - zero or the number of crottles is zero. Note that they - therefore also can both be zero. + zero or the number of crottles is zero in a truck. \item Makes sure that skipples are only in the first two cooled trucks by stating that if the truck number not one or two the number of skipples is zero. @@ -71,39 +73,31 @@ all pallets. \setcounter{enumi}{6} \item Makes sure that all mandatory pallets are transported by summing over all trucks and assuring the number of the - pallets of that type is exactly $n(r)$. Note that this - should hold or that the current pallet is a prittle - pallet since we do not have a limit on prittles. + pallets of that type is exactly $n(r)$. \end{enumerate} \end{itemize} \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. +Listing~\ref{listing:a1.smt}. The maximization is done by incrementing a +special variable called \texttt{} which is an instantiation of $n(p)$. +When the iteration yields unsat we know that the current number minus one is +the maximum amount of prittles the trucks can carry. The maximization is done +with a bash script shown in Listing~\ref{listing:1.bash}. -\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} +\lstinputlisting[language=bash, + caption={Iteratively find the largest solution for problem 1}, + label={listing:1.bash}]{src/a1.bash} \subsection{Solution} -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}. +The bash script finds and shows the maximal solution of $18$ prittles. Finding +this solution takes less then $0.12$ seconds and is shown in Table~\ref{tab:s1}. \begin{table}[H] \begin{tabular}{|l|lllll|l|l|} \hline - Truck & Nuzzles & Prittles & Skipples & Crottles & Dupples & Weight & Pallets\\ + 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\\ @@ -115,6 +109,6 @@ to be deliverd is $18$. When we rerun the solution with $18$ prittles and the total & 4 & 18 & 8 & 10 & 5 & &\\ \hline \end{tabular} - \caption{Solution table for problem 1} - \label{tab:s1} + \caption{Solution visualization for problem 1} +\label{tab:s1} \end{table} diff --git a/ar/assignments/2.tex b/ar/assignments/2.tex index f4789d8..7fd4047 100644 --- a/ar/assignments/2.tex +++ b/ar/assignments/2.tex @@ -6,97 +6,116 @@ 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 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). + 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} } +\newpage \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. +For every component $c_{i}$ for $i\in PC\cup RC$ where $PC=\{1,\ldots,3\}$ and +$RC=\{4,\ldots,11\}$ we define a width, a height, an $x$ and a $y$ variables +$c_{i}w$, $c_{i}h$, $c_{i}x$ and $c_{i}y$. $c_ih$ does not necessarily have the +specified height of the components since the components may be rotated. For the +specified width and height we introduce the functions $h(c)$ and $w(c)$ that +return the specified width and height. + +This leads to the following formalization. \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_jh0\wedge 22-c_{i}h\geq c_{i}y>0\\ + & \wedge \bigwedge_{j\in PC\cup RC}\Bigl(j\geq i\\ + \nonumber & \qquad\qquad\qquad \vee c_{i}x>c_{j}x+c_{j}w\\ + \nonumber & \qquad\qquad\qquad \vee c_{i}x+c_{j}wc_{j}y+c_{j}h\\ + \nonumber & \qquad\qquad\qquad + \vee c_{i}y+c_{j}h17\\ - \nonumber & \vee c_jx+\frac{c_jw}{2}-c_ix+\frac{c_iw}{2}>17\\ - \nonumber & \vee c_iy+\frac{c_ih}{2}-c_jy+\frac{c_jh}{2}>17\\ - \nonumber & \vee c_jy+\frac{c_jh}{2}-c_iy+\frac{c_ih}{2}>17\Biggr)\wedge\\ + \nonumber & \vee c_{i}x+\nicefrac{c_{i}w}{2}- + c_{j}x+\nicefrac{c_{j}w}{2}>17\\ + \nonumber & \vee c_{j}x+\nicefrac{c_{j}w}{2}- + c_{i}x+\nicefrac{c_{i}w}{2}>17\\ + \nonumber & \vee c_{i}y+\nicefrac{c_{i}h}{2}- + c_{j}y+\nicefrac{c_{j}h}{2}>17\\ + \nonumber & \vee c_{j}y+\nicefrac{c_{j}h}{2}- + c_{i}y+\nicefrac{c_{i}h}{2}>17\Biggr)\wedge\\ \bigwedge_{i\in RC}\bigvee_{j\in PC}\neg\Biggl( - & (c_ix-1>c_jx+c_jw\\ - \nonumber & \vee c_ix+1+c_jwc_jy+c_jh\\ - \nonumber & \vee c_iy+1+c_jhc_{j}x+c_{j}w\\ + \nonumber & \vee c_{i}x+1+c_{j}wc_{j}y+c_{j}h\\ + \nonumber & \vee c_{i}y+1+c_{j}h0\wedge j_{i}+ij_{k}+k\Biggr)\\ + & \wedge \bigwedge_{i\in J'}\bigwedge_{k\in J'} + i=j\vee j_{i}>j_{k}+k \vee j_{i}+i/$i/g" a1.smt | yices-smt) = "sat" ]; do + i=$((i+1)) +done +sed "s//$((i-1))/g" a1.smt | yices-smt -m diff --git a/ar/assignments/src/1.smt b/ar/assignments/src/a1.smt similarity index 100% rename from ar/assignments/src/1.smt rename to ar/assignments/src/a1.smt diff --git a/ar/assignments/src/a2.bash b/ar/assignments/src/a2.bash new file mode 100644 index 0000000..5462573 --- /dev/null +++ b/ar/assignments/src/a2.bash @@ -0,0 +1 @@ +python3 a2.py | yices-smt -m diff --git a/ar/assignments/src/2.py b/ar/assignments/src/a2.py similarity index 100% rename from ar/assignments/src/2.py rename to ar/assignments/src/a2.py diff --git a/ar/assignments/src/a3.bash b/ar/assignments/src/a3.bash new file mode 100644 index 0000000..115f1fd --- /dev/null +++ b/ar/assignments/src/a3.bash @@ -0,0 +1,5 @@ +i=1 +while [ $(python3 a3.py $i | yices-smt) = "unsat" ]; do + i=$((i+1)) +done +python3 a3.py $i | yices-smt -m diff --git a/ar/assignments/src/a3.py b/ar/assignments/src/a3.py new file mode 100644 index 0000000..a295c8d --- /dev/null +++ b/ar/assignments/src/a3.py @@ -0,0 +1,47 @@ +#!/usr/bin/env python3 +import sys + +if len(sys.argv) != 2: + print("usage: {} maxjobstart".format(sys.argv[0])) + exit() + +maxjobstart = sys.argv[1] +jobs = 12 +J = range(1, jobs+1) +Jprime = {5, 7, 10} +pi = { + 3: {1,2}, + 5: {3,4}, + 7: {3,4,6}, + 9: {5,8}, + 11: {10}, + 12: {9,11} +} + +# Print preamble +print("(benchmark a4.smt") +print(":logic QF_UFLIA") + +# Print variables +print(":extrafuns (") +for i in J: + print("(j{} Int)".format(i), end=' ') +print("\n)") + +print(":formula") +print("(and") +for i in J: + # Make sure the times are positive and within the bound + print("(> j{0} 0) (<= (+ j{0} {0}) {1})".format(i, maxjobstart)) + # Make sure the dependencies are done when a task is scheduled + for k in pi.get(i, {}): + print("(>= j{0} (+ j{1} {1}))".format(i, k)) +# Make sure the shared resources are not used by two tasks at once +for i in Jprime: + for k in Jprime: + if i != k: + print("(or (>= j{0} (+ j{1} {1}))".format(i,k), end=' ') + print("(<= (+ j{0} {0}) j{1}))".format(i,k)) + +# Close the and,benchmark parenthesis +print("))") diff --git a/ar/assignments/src/a4.bash b/ar/assignments/src/a4.bash new file mode 100644 index 0000000..7a5211d --- /dev/null +++ b/ar/assignments/src/a4.bash @@ -0,0 +1,5 @@ +i=1 +while [ $(python3 a4.py $i | yices-smt) = "unsat" ]; do + i=$((i+1)) +done +python3 a3.py $((i-1)) | yices-smt -m diff --git a/ar/assignments/src/4.py b/ar/assignments/src/a4.py similarity index 100% rename from ar/assignments/src/4.py rename to ar/assignments/src/a4.py