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
+++ /dev/null
-\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}}
+++ /dev/null
-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).
(<= (+ (* 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 t5p) (= 0 t5c))
(or (= 0 t6p) (= 0 t6c))
- (= t3s 0)
- (= t4s 0)
- (= t5s 0)
- (= t6s 0)
-
(<= t1d 1)
(<= t2d 1)
(<= t3d 1)
(<= 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) <REP>)
)
)
repositories / master.git / commitdiff