From: Mart Lubbers Date: Tue, 20 Oct 2015 08:39:34 +0000 (+0200) Subject: ar ex1 done X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=594d460e4068a28a70434429a3fa3b4497ef9287;p=master.git ar ex1 done --- diff --git a/ar/assignments/1.tex b/ar/assignments/1.tex index f45e8b4..51fc39e 100644 --- a/ar/assignments/1.tex +++ b/ar/assignments/1.tex @@ -19,43 +19,61 @@ 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[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$$ +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 +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. -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)$$ +\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}\Biggl( + & r=p\vee\left(\sum^{T}_{i=1}t_ir\right)=n(r)\Biggr) +\end{align} -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. +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. +\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 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 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. + \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. + \end{enumerate} + \item \textbf{Pallets} + \begin{enumerate} + \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. + \end{enumerate} +\end{itemize} \subsection{SMT format solution} The formula is easily convertable to SMT format and is listed in diff --git a/ar/assignments/ar.aux b/ar/assignments/ar.aux deleted file mode 100644 index f75a08e..0000000 --- a/ar/assignments/ar.aux +++ /dev/null @@ -1,25 +0,0 @@ -\relax -\@writefile{toc}{\contentsline {section}{\numberline {1}Problem 1}{1}} -\@writefile{toc}{\contentsline {subsection}{\numberline {1.1}Formal definition}{1}} -\@writefile{toc}{\contentsline {subsection}{\numberline {1.2}SMT format solution}{2}} -\newlabel{listing:1bash}{{1}{2}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {1}Iteratively find the largest solution}{2}} -\@writefile{toc}{\contentsline {subsection}{\numberline {1.3}Solution}{2}} -\@writefile{toc}{\contentsline {section}{\numberline {2}Problem 4}{3}} -\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Formal definition}{3}} -\@writefile{toc}{\contentsline {paragraph}{Precondition}{3}} -\newlabel{eq:4pre}{{1}{3}} -\@writefile{toc}{\contentsline {paragraph}{Program}{3}} -\newlabel{eq:4pro}{{2}{3}} -\@writefile{toc}{\contentsline {paragraph}{Postcondition}{3}} -\newlabel{eq:4pst}{{3}{3}} -\@writefile{toc}{\contentsline {paragraph}{Total}{3}} -\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}SMT format solution}{3}} -\newlabel{listing:4bash}{{2}{3}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {2}Iteratively find the shortest solution}{3}} -\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}Solution}{4}} -\@writefile{toc}{\contentsline {section}{\numberline {3}Appendix}{4}} -\newlabel{listing:a1.smt}{{3}{5}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {3}a1.smt}{5}} -\newlabel{listing:4.py}{{4}{6}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {4}a4.py}{6}} diff --git a/ar/assignments/ar.fmt b/ar/assignments/ar.fmt deleted file mode 100644 index ebcbaee..0000000 Binary files a/ar/assignments/ar.fmt and /dev/null differ diff --git a/ar/assignments/ar.log b/ar/assignments/ar.log deleted file mode 100644 index 89ca6cb..0000000 --- a/ar/assignments/ar.log +++ /dev/null @@ -1,77 +0,0 @@ -This is pdfTeX, Version 3.14159265-2.6-1.40.15 (TeX Live 2015/dev/Debian) (preloaded format=ar 2015.10.19) 19 OCT 2015 20:25 -entering extended mode - restricted \write18 enabled. - %&-line parsing enabled. -**ar -(./ar.tex -LaTeX2e <2014/05/01> -Babel <3.9l> and hyphenation patterns for 79 languages loaded. -(./ar.aux) -\openout1 = `ar.aux'. - -LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 2. -LaTeX Font Info: ... okay on input line 2. -LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 2. -LaTeX Font Info: ... okay on input line 2. -LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 2. -LaTeX Font Info: ... okay on input line 2. -LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 2. -LaTeX Font Info: ... okay on input line 2. -LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 2. -LaTeX Font Info: ... okay on input line 2. -LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 2. -LaTeX Font Info: ... okay on input line 2. -\c@lstlisting=\count107 - (./1.tex -Underfull \hbox (badness 10000) in paragraph at lines 3--6 - - [] - -LaTeX Font Info: Try loading font information for OMS+cmr on input line 7. -(/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd -File: omscmr.fd 2014/09/29 v2.5h Standard LaTeX font definitions -) -LaTeX Font Info: Font shape `OMS/cmr/m/it' in size <10> not available -(Font) Font shape `OMS/cmsy/m/n' tried instead on input line 7. - [1] -(/usr/share/texlive/texmf-dist/tex/latex/listings/lstlang1.sty -File: lstlang1.sty 2014/09/06 1.5e listings language file -) -(/usr/share/texlive/texmf-dist/tex/latex/listings/lstlang1.sty -File: lstlang1.sty 2014/09/06 1.5e listings language file -) -LaTeX Font Info: Try loading font information for OML+cmr on input line 72. - -(/usr/share/texlive/texmf-dist/tex/latex/base/omlcmr.fd -File: omlcmr.fd 2014/09/29 v2.5h Standard LaTeX font definitions -) -LaTeX Font Info: Font shape `OML/cmr/m/n' in size <8> not available -(Font) Font shape `OML/cmm/m/it' tried instead on input line 72. -LaTeX Font Info: Font shape `OMS/cmr/m/n' in size <8> not available -(Font) Font shape `OMS/cmsy/m/n' tried instead on input line 72. -) (./2.tex) (./3.tex) -(./4.tex [2] -Overfull \hbox (38.59985pt too wide) detected at line 46 -[] [] - [] - -[3]) (./a.tex [4] -(/usr/share/texlive/texmf-dist/tex/latex/listings/lstlang1.sty -File: lstlang1.sty 2014/09/06 1.5e listings language file -) -(/usr/share/texlive/texmf-dist/tex/latex/listings/lstlang2.sty -File: lstlang2.sty 2014/09/06 1.5e listings language file -) (./src/1.smt) -[5] (/usr/share/texlive/texmf-dist/tex/latex/listings/lstlang1.sty -File: lstlang1.sty 2014/09/06 1.5e listings language file -) (./src/4.py)) [6] (./ar.aux) ) -Here is how much of TeX's memory you used: - 807 strings out of 491017 - 9506 string characters out of 6109189 - 274834 words of memory out of 5000000 - 6326 multiletter control sequences out of 15000+600000 - 14800 words of font info for 52 fonts, out of 8000000 for 9000 - 1141 hyphenation exceptions out of 8191 - 35i,7n,51p,203b,1306s stack positions out of 5000i,500n,10000p,200000b,80000s - -Output written on ar.dvi (6 pages, 37960 bytes). diff --git a/ar/assignments/ar.pdf b/ar/assignments/ar.pdf deleted file mode 100644 index 8fa46dd..0000000 Binary files a/ar/assignments/ar.pdf and /dev/null differ diff --git a/ar/assignments/src/1.smt b/ar/assignments/src/1.smt index 77871e1..cf5342e 100644 --- a/ar/assignments/src/1.smt +++ b/ar/assignments/src/1.smt @@ -31,11 +31,6 @@ (<= (+ (* 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)) @@ -43,11 +38,6 @@ (or (= 0 t5p) (= 0 t5c)) (or (= 0 t6p) (= 0 t6c)) - (= t3s 0) - (= t4s 0) - (= t5s 0) - (= t6s 0) - (<= t1d 1) (<= t2d 1) (<= t3d 1) @@ -55,6 +45,16 @@ (<= t5d 1) (<= t6d 1) + (= t3s 0) + (= t4s 0) + (= t5s 0) + (= t6s 0) + + (= (+ 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) + (>= (+ t1p t2p t3p t4p t5p t6p) ) ) )