Part 4 problem definition and horrible implementation

1 files changed, 29 insertions, 2 deletions

diff --git a/part2.tex b/part2.tex
index e6b11e9..c30489c 100644
--- a/part2.tex
+++ b/part2.tex
@@ -447,7 +447,7 @@ Running this input through \textit{prover9} generated the following proofs for \
 
 \textit{prover9} was not able to prover that $x * y = y * x$ holds for all finite groups. Therefor, we ran \ref{itm:logic_b_4} through \textit{mace4} to find the smallest group $G(I, *, inv)$ for which $x * y \neq y * x$.
 The following input was used:
-\begin{verbatim}
+\begin{lstlisting}
 formulas(sos).
 	(x*(y*z)=(x*y)*z).
 	(x*I=x).
@@ -457,7 +457,7 @@ end_of_list.
 formulas(goals).
 	all x all y (x*y=y*x).
 end_of_list.
-\end{verbatim}
+\end{lstlisting}
 After running this input through \textit{mace4}, we retrieved the following finite group $G(I, *, inv)$:
 \begin{verbatim}
  I: 0
@@ -489,5 +489,32 @@ single solutions of simply specified puzzles like sudokus. In case of doubt
 please contact the lecturer.
 
 \subsection*{Solution:}
+We decided to choose a highscool room scheduling problem.
+
+\begin{itemize}
+ \item The highschool has $n$ classes
+ \item The highschool only has $ceil(n * 0.7)$ rooms though
+ \item Every class has to attend at least 1040 hours a year, which is equivalent to 26 hours per week
+ \item Every day contains 8 timeslots of 1 hour, in which lectures can take place
+ \item Lectures take place 5 days a week, giving a total of 40 timeslots per week
+ \item There are 10 different courses:\\\\
+ \begin{tabular}{l c r}
+  English	  &	3 hours per week & \\
+  German	  &	2 hours per week & \\
+  Spanish	  &	2 hours per week & \\ 
+  Math	  	  &	3 hours per week & \\
+  Physics	  &	3 hours per week & \\
+  Chemistry 	  &	3 hours per week & \\ 
+  Biology	  &	3 hours per week & \\ 
+  Art	  	  &	1 hour per week	 & \\ 
+  Geography 	  &	3 hours per week & \\
+  History	  &	3 hours per week & \\
+ \end{tabular}
+\end{itemize}
+
+We want to schedule the rooms in such way that every class attends all required lessons per week, and the total amount of free hours inbetween 2 lectures is minimized.
+
+\subsubsection*{Solution:}
+
 
 \end{document}