\documentclass[12pt]{article}
\usepackage{a4wide}
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{epic}
\usepackage{graphicx}
\usepackage{gensymb}
\usepackage{listings}
\usepackage{tikz}
\usepackage{amsmath}
\usepackage{hyperref}
\usepackage{float}
%\pagestyle{empty}
\newcommand{\tr}{\mbox{\sf true}}
\newcommand{\fa}{\mbox{\sf false}}
\newcommand{\bimp}{\leftrightarrow}     % bi-implication

\title{Assignment part 2 for Automated Reasoning 2IMF25}
\author{%
    Peter Wu (0783206)\\
    \texttt{s.p.wu@student.tue.nl}
\and
    Koen van der Heijden (0807929)\\
    \texttt{k.p.l.v.d.heijden@student.tue.nl}
}
\date{\today}

\begin{document}
\maketitle

\section*{Problem: food delivery}
Four non-self-supporting villages A, B, C and D in the middle of nowhere consume
one food package each per time unit. The required food packages are delivered by
a truck, having a capacity of 240 food packages. The truck has to pick up its
food packages at location S containing an unbounded supply. The locations of
this supply location and the villages and the roads between them are shown in
the following picture. Here every number indicates a distance, more precisely,
the number of time units the truck needs to travel from one village to another,
including loading and delivering. The villages only have a limited capacity to
store food packages: for A this capacity is 120, for B and D it is 160, and for
C it is 100. Initially, the truck is in S and is fully loaded, and in each of
the four villages there are 80 food packages.

\begin{figure*}
\centering
\begin{tikzpicture}[scale=.2]
\node[circle,draw] (A) at (0,0) {A};
\node[circle,draw] (B) at (17,0) {B};
\node[circle,draw] (C) at (9.794,-6.934) {C};
\node[circle,draw] (D) at (26.824,-17.421) {D};
\node[circle,draw] (S) at (-3.046,-14.687) {S};

\draw
    (A) edge node[above]        {17} (B)
    (A) edge node[above left]   {15} (S)
    (A) edge node[above right]  {12} (C)
    (S) edge node[below right]  {15} (C)
    (B) edge node[above left]   {10} (C)
    (B) edge node[above right]  {20} (D)
    (C) edge node[below left]   {20} (D)
    ;
\end{tikzpicture}
\end{figure*}

\begin{enumerate}
\item[(a)] Show that it is impossible to deliver food packages in such a way
that each of the villages consumes one food package per time unit forever.
\item[(b)] Show that this is possible if the capacity of the truck is increased
to 260 food packages. (Note that a finite graph contains an infinite path
starting in a node $v$ if and only if there is a path from $v$ to a node $w$ for
which there is a non-empty path from $w$ to itself.)
\end{enumerate}

\subsection*{Solution:}
\subsubsection*{(a)}

\subsubsection*{(b)}


\section*{Problem: Nondeterministic finite automaton (NFA)}
Let an NFA be defined as in Wikipedia \\
\url{https://en.wikipedia.org/wiki/Nondeterministic_finite_automaton}\\
Find an NFA $M$ over $\sum = \{a, b\}$ with the least possible number of states
for which the only non-empty words in $L(M)$ of length $<$ 5 are $aa$, $bb$,
$aba$, $baa$, $abab$, $babb$ and $bbba$.

\subsection*{Solution:}


\section*{Problem: }
The goal of this problem is to exploit the power of the recommended tools rather
than elaborating the questions by hand.
\begin{enumerate}
\item[(a)] For a binary operator a we have the idempotence, commutativity and
associativity rule, that is, the three rewrite rules
\[
a(x, x) \to x, a(x, y) \to a(y, x), a(x, a(y, z)) \to a(a(x, y), z).
\]
Figure out whether $a(p, a(q, a(p, a(q, a(p, a(q, p))))))$ rewrites to $a(p, q)$
in a finite number of steps, for constants $p$, $q$.
\item[(b)] In mathematics, a group is defined to be a set $G$ with an element
$I \in G$, a binary operator $*$ and a unary operator $inv$ satisfying
\[
    x * (y * z) = (x * y) * z,\ x * I = x \text{ and } x * inv(x) = I,
\]
for all $x, y, z \in G$. Determine whether in every group each of the four properties
\[
    I * x = x,\ inv(inv(x)) = x,\ inv(x) * x = I \text{ and } x * y = y * x
\]
holds for all $x, y \in G$. If a property does not hold, determine the size of
the smallest finite group for which it does not hold.
\end{enumerate}

\subsection*{Solution:}
\subsubsection*{(a)}

\subsubsection*{(b)}


\section*{Problem: }
Give a precise description of a non-trivial problem of your own choice, and
encode this and solve it by one of the given programs.
Here `trivial problems' include both minor modifications of earlier problems and
single solutions of simply specified puzzles like sudokus. In case of doubt
please contact the lecturer.

\subsection*{Solution:}

\end{document}