path: root/part2.tex

\documentclass[12pt]{article}
\usepackage{a4wide}
\usepackage{latexsym}
\usepackage{amsmath, amssymb}
\usepackage{epic}
\usepackage{graphicx}
\usepackage{gensymb}
\usepackage[table]{xcolor}
\usepackage{listings}
\usepackage{tikz}
\usetikzlibrary{automata,positioning}
\usepackage{hyperref}
\usepackage{float}
\usepackage{enumitem}
%\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)}
We generalize the problem as a graph $G=(V,E)$ where the vertices $V$ represent
villages and the supply location (denoted $S$) and edges $E$ represent the paths
between the vertices. We also define a weight function $cost : E \to
\mathbb{N}$. For brevity, we denote the villages (without the supply location)
by $V'=V \setminus \{S\}$.
The process of transporting and delivering food packages is modelled as state
transitions. The state after $0 \leq j \leq m$ steps consists of:
\begin{itemize}
\item Current location of truck: $l_j \in V$.
\item Remaining food stock at village $i \in V'$, denoted by $s_{i,j}$.
\item Remaining food stock in truck, denoted by $s_{T,j}$.
\end{itemize}

The truck (denoted as $T$) and villages have maximum capacities, let these be
defined by the function $capacity : (V' \cup \{T\}) \to \mathbb{N}$.
With these definitions in place, let us define the initial state for the
specific scenario where the truck starts at the supply location:
\begin{align}
\label{eq:food1}
l_0 = S
\land \bigwedge_{i \in V'} s_{i,0} = 80
\land s_{T,0} = capacity(T)
\end{align}

Now require that the truck capacity never drops below zero and that villages
always have some food to consume and are never overstocked:
\begin{align}
\label{eq:food2}
\bigwedge_{j=0}^m
0 \leq s_{T,j}
\land
\bigwedge_{i \in V' } 0 \leq s_{i,j} \leq capacity(i)
\end{align}

Finally we add the constraints for state transitions. At every state, any of
the enabled transitions can be taken (if this is not possible for any state,
then indeed it is impossible to deliver food packages in such a way without
starving some villages).
We add ingredients to express:
\begin{itemize}
\item Part~\ref{eq:food3}:
whether the target is reachable from the previous location.
\item Part~\ref{eq:food4}:
whether the village has sufficient food for consumption while the truck travels.
\item Part~\ref{eq:food5}:
villages (other than the target) eat some food (but are not restocked).
Note that this covers all villages if the next target is the supply location, so
the village stock $s_{i,j}$ is always defined.
\item Part~\ref{eq:food6}:
if target is village, eat some and optionally restock the village (as long as
the truck has some stock). For brevity, we define $drop(j) = s_{T,j-1} -
s_{T,j}$, expressing how much food is unloaded from the truck and dropped into
the village.
\item Part~\ref{eq:food7}:
if target is supply location, the truck is always fully restocked. (This and the
previous part ensures that $s_{T,j}$ is always defined.)
\end{itemize}
\begin{align}
\label{eq:food3}
\bigwedge_{j=1}^m
\bigvee_{(x, y) \in E}
&(l_{j-1}, l_j) = (x, y)
%
\\\label{eq:food4}
&\land
\bigwedge_{i \in V'} s_{i,j-1} \geq cost(x, y)
%
\\\label{eq:food5}
&\land
\bigwedge_{i \in V', i \neq y}
s_{i,j} = s_{i,j-1} - cost(x, y)
%
\\\label{eq:food6}
&\land
y \neq S \implies
    (s_{i,j} = s_{i,j-1} - cost(x, y) + drop(j)
    \land
    drop(j) \geq 0
    )
%
\\\label{eq:food7}
&\land
y = S \implies
s_{T,j} = capacity(T)
\end{align}

With the given path travelling costs $cost$, truck and villages $V$ and their
capacities $capacity$, we are able to build the route that the truck travels,
parameterized by the number of visited locations $m$.
We wrote a generator program in Python that outputs a SMT corresponding to
conjunction of the above ingredients (mapping $V=\{S,A,B,C,D\}$ to the indices
$0,1,2,3,4$), this is shown in Listing~\ref{lst:food}.

We picked (arbitrary) $m=30$ and applied Z3 to the generated SMT which resulted
in \texttt{unsat} after four seconds. Then we applied binary search and found
that for $m=22$ the output is still \texttt{unsat} (after four seconds)
while for $m=21$ a solution is found within a second. This shows that a valid
route with 21 visited locations can be obtained and that no route exists such
that 22 locations are visited. It is thus impossible to deliver food packages
in such a way that each of the villages can consume one food packge forever.

\begin{lstlisting}[
    caption={Generated SMT program for food delivery problem (a) with $m=30$.},
    label={lst:food},basicstyle=\scriptsize,language=lisp
]
(benchmark test.smt
:logic QF_UFLIA
:extrafuns (
(s0_0 Int) (s1_0 Int) ... (s4_0 Int) (l0 Int)
...
)
:formula (and
(= l0 0)
(= s1_0 80) (= s2_0 80) (= s3_0 80) (= s4_0 80) (= s0_0 240) (>= s0_0 0)
(>= s1_0 0) (<= s1_0 120) (>= s2_0 0) (<= s2_0 160)
(>= s3_0 0) (<= s3_0 100) (>= s4_0 0) (<= s4_0 160)
...
(or (and (= l0 0) (= l1 1)
         (>= s1_0 15) (>= s2_0 15) (>= s3_0 15) (>= s4_0 15)
         (>= (- s0_0 s0_1) 0)
         (= s1_1 (+ (- s1_0 15) (- s0_0 s0_1)))
         (= s2_1 (- s2_0 15))
         (= s3_1 (- s3_0 15))
         (= s4_1 (- s4_0 15)))
    ...
    (and (= l0 1) (= l1 0)
         (>= s1_0 15) (>= s2_0 15) (>= s3_0 15) (>= s4_0 15)
         (= s1_1 (- s1_0 15))
         (= s2_1 (- s2_0 15))
         (= s3_1 (- s3_0 15))
         (= s4_1 (- s4_0 15))
         (= s0_1 240))
    ...
) ...))
\end{lstlisting}

\subsubsection*{(b)}
In the solution to (a) we showed that an infinite series with the previous
requirements is already impossible. When the maximum truck capacity is increased
from $capacity(T)=240$ to $capacity(T)=260$, we shall add another ingredient
to check that villages can indeed consume food forever.

We do so by trying to find a state $k_1 \leq m$ where the stock of the truck and
the stock of each village is at least as high as a previous state $0 \leq k_0$
at the same location:
\begin{align}
\label{eq:food8}
\bigvee_{0 \leq k_0 < k_1 \leq m}
k_0 < k_1 \land l_{k_0} = l_{k_1} \land
s_{T,k_0} \leq s_{T,k_1}
\land
\bigwedge_{i \in V'} s_{i,k_0} \leq s_{i,k_1}
\end{align}

The SMT output generated by the augmented program includes two new variables and
adds Part~\ref{eq:food8} to the conjunction as shown in Listing~\ref{lst:foodB}.
For $m=12$ we obtained \texttt{unsat} after 9 seconds (showing that a loop was
not yet obtained) while for $m=13$ a satisfying assignment was found in 10
seconds. The resulting assignment is shown in Table~\ref{tbl:foodB}. Indeed, now
it is possible to deliver food in a way such that every village can consume food
forever.

\begin{lstlisting}[
    caption={Generated SMT program for food delivery problem (b) with $m=13$.},
    label={lst:foodB},basicstyle=\scriptsize,language=lisp
]
(benchmark test.smt
:logic QF_UFLIA
:extrafuns ( ... (k0 Int) (k1 Int))
:formula (and ...
(or (and (= k0 1) (= k1 2) (= l1 l2) (<= s0_1 s0_2) ... (<= s4_1 s4_2))
    (and (= k0 1) (= k1 3) (= l1 l3) (<= s0_1 s0_3) ... (<= s4_1 s4_3))
    ...
    (and (= k0 12) (= k1 13) (= l12 l13) (<= s0_12 s0_13) ... (<= s4_12 s4_13)))
))
\end{lstlisting}

\begin{table}[H]
\centering
\footnotesize
\begin{tabular}{r|r|rrrr|c}
    & \multicolumn{4}{c}{Stock at location} & \\
 $j$&     T &     A &     B &    C &      D & $l_j$ \\
\hline
  0 &   260 &    80 &    80 &    80 &    80 & S \\
  1 &   222 &\bf103 &    65 &    65 &    65 & A \\
  2 &   181 &    86 &\bf 89 &    48 &    48 & B \\
\rowcolor{lightgray}
  3 &    52 &    66 &    69 &    28 &\bf157 & D \\ % PAIR
  4 &     3 &    46 &    49 &\bf 57 &   137 & C \\
  5 &   260 &    31 &    34 &    42 &   122 & S \\
  6 &   219 &\bf 57 &    19 &    27 &   107 & A \\
  7 &    62 &    40 &\bf159 &    10 &    90 & B \\
  8 &     1 &    30 &   149 &\bf 61 &    80 & C \\
  9 &   260 &    15 &   134 &    46 &    65 & S \\
 10 &   144 &\bf116 &   119 &    31 &    50 & A \\
 11 &   260 &   101 &   104 &    16 &    35 & S \\
 12 &   213 &    86 &    89 &\bf 48 &    20 & C \\
\rowcolor{lightgray}
 13 &    56 &    66 &    69 &    28 &\bf157 & D \\ % PAIR
\end{tabular}
\caption{\label{tbl:foodB}The solution calculated by z3 for $m=13$, showing the
initial and following states (consisting of truck and village stock and current
location $l_j$) after $j$ transitions. State $j=13$ has greater or equal stocks
than state $j=13$ at location D.}
\end{table}

\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:}
Model the NFA as $M = \{Q, \Sigma, \Delta, q_0, F\}$ where $Q=\{q_0, \ldots,
q_{m-1}\}$ is the set of states, $\Sigma$ is the alphabet, $\Delta$ is the
transition function $\Delta: Q \times \Sigma \to P(Q)$, $q_0 \in Q$ is the
initial state and $F \subseteq Q$ is the set of final (accepting) states. The
list of accepted words is $L(M)$.
Let $S_{i,j}$ be the mapping to a state in $Q$ from character index $0 \leq j$
of word $w_i \in L(M)$.

For the given scenario, we also define \emph{bad} words (words with a length
smaller than five, but not in the accepted language):
\begin{align}
    W' = \{ w |
        w \in \Sigma^*
        \land 1 \leq \#w \leq 4
        \land w \not\in L(M)
    \}
\end{align}

To solve the problem, we first try to find a NFA for a $m$ states and then
gradually decrement it until we obtain \texttt{unsat}. An overview of our
approach (a more detailed description will follow):
\begin{enumerate}
\item For each valid word $w_i$ in $L(M)$:
    \begin{enumerate}
        \item Add new states for each letter $j$ of the word $w_i$: $S_{i,j}$.
            Note that these states use different variables ($S$) than the states
            of the NFA ($Q$).
        \item Add new transitions to the formula, starting from the common
            initial state $q_0$. The next states are $S_{i,0}$, $S_{i,1}$, etc.
            This expresses that the input $w_i$ is indeed accepted by $M$.
        \item Add a constraint to the formula to express that the last letter
            ends up in a final state.
    \end{enumerate}
\item For every \emph{bad} word, add an implication to the formula: if
    the word exists, then the last state of this word must not be accepting.
\item Finally map each of the states $S_{i,j}$ to a state in $Q$ via
    conjunctions (for each word) consisting of disjunctions (for each state
    $S_{i,j}$) that try to match with any state in $Q$.
\end{enumerate}

First we require that every non-empty word $w_i$ is indeed accepted as input: a
path exists from the initial state to the final state, following each letter one
by one:
\begin{align}
    \bigwedge_{w_i \in L(M)}
    \Delta(q_0, w_{i,0}) = S_{i,0}
    \land
    (\bigwedge_{j=1}^{\#w_i}
    \Delta(S_{i,j-1}, w_{i,j-1}) = S_{i,j})
    \land
    S_{i,\#w_i} \in F
\end{align}

The above expression assigns values to $S_{i,j}$, making it easier to put
restrictions on the ``characters'' of each word (for example, requiring that the
word originates from the initial state $q_0$ and that the last state is
accepting). To make it more useful, it should be mapped somehow to $Q$ so we can
obtain the desired NFA. For simplicity, let's assume that each character can be
assigned to any state in $Q$:
\begin{align}
    \bigwedge_{w_i \in L(M)}
    \bigwedge_{j=0}^{\#w_i}
    \bigvee_{q \in Q} S_{i,j} = q
\end{align}
Note that this includes all possible states in $Q$, including the initial state
$q_0$. Being the initial state does not exclude the state from receiving
incoming transitions.

Finally we have to exclude transitions, otherwise even a single, initial and
final state would be permitted (with transitions to itself). Since loops are
possible and transitions to any earlier state can occur, it is not sufficient
to (for example) just exclude input that differ only in the trailing character.
Therefore we check all possible \emph{bad words} $W'$.
\begin{align}
    \bigwedge_{w_i \in W'}
        \Delta(q_0, w_{i,0}) = T_{i,0}
        \land
        (\bigwedge_{j=1}^{\#w_i}
        \Delta(T_{i,j-1}, w_{i,j-1}) = T_{i,j})
    \implies
    T_{i,\#w_i} \not\in F
\end{align}

\textbf{Implementation notes}:
we combined the above three ingredients into a conjunction and implemented it
via a Python script that generates a SMT. To allow for concise SMT without
exploding in the number of variables, we used functions. These have no limits in
their domain or range so we have to add manual checks for these. For the states
$S_{i,j}$ that match good words and for states $T_{i,j}$ that match bad words,
we implemented range checks like $T_{i,j} \in Q$.
(Actually, we set $q_i = i$ for $0 \leq i < m$, so the above range check simply
checks whether the values are within that range.)
These checks are either added to the global formula (for the good words) or
before the implication (for the bad words).

The generated SMT program has a shape which is shown in Listing~\ref{lst:nfa}.
It runs within a second, even for $m=1000$. By gradually reducing it as stated
before, we found that for $m=7$ no automaton was found (\texttt{unsat}) but for
$m=8$, a valid result was obtained (see Figure~\ref{fig:nfa}). Note that the Z3
output (Listing~\ref{lst:nfaZ3}) contains out-of-range and out-of-domain values
because the $trans$ ($\Delta$) function for example is used with arbitrary
values before the implication. When an implication evaluates to false, then the
solver still keeps the garbage values even if it remains unused (its exact value
does not influence the result of the evaluation).

\begin{lstlisting}[
    caption={Generated SMT program for NFA with $m=8$.},
    label={lst:nfa},basicstyle=\scriptsize,language=lisp
]
(benchmark test.smt
:logic QF_UFLIA
:extrafuns (
(q0 Int) (q1 Int) (q2 Int) (q3 Int) (q4 Int) (q5 Int) (q6 Int) (q7 Int)
(s0_0 Int) (s0_1 Int) (s1_0 Int) (s1_1 Int) (s2_0 Int) (s2_1 Int) (s2_2 Int)
(s3_0 Int) (s3_1 Int) (s3_2 Int) (s4_0 Int) (s4_1 Int) (s4_2 Int) (s4_3 Int)
(s5_0 Int) (s5_1 Int) (s5_2 Int) (s5_3 Int) (s6_0 Int) (s6_1 Int) (s6_2 Int)
(s6_3 Int)
(trans Int Int Int)
(final Int Bool)
)
:formula (and
(= q0 0) (= q1 1) (= q2 2) (= q3 3) (= q4 4) (= q5 5) (= q6 6) (= q7 7)
(= (trans q0 0) s0_0)
(= (trans s0_0 0) s0_1)
(final s0_1)
...
(= (trans q0 1) s6_0)
(= (trans s6_0 1) s6_1)
(= (trans s6_1 1) s6_2)
(= (trans s6_2 0) s6_3)
(final s6_3)
(=> (and (>= (trans q0 0) 0) (< (trans q0 0) 8)) (not (final (trans q0 0))))
(=> (and (>= (trans q0 1) 0) (< (trans q0 1) 8)) (not (final (trans q0 1))))
(=> (and (>= (trans          q0  0) 0) (< (trans          q0  0) 8)
         (>= (trans (trans q0 0) 1) 0) (< (trans (trans q0 0) 1) 8))
    (not (final (trans (trans q0 0) 1))))
...
(or (= q0 s0_0) (= q1 s0_0) ... (= q7 s0_0))
...
(or (= q0 s6_3) (= q1 s6_3) ... (= q7 s6_3))
))
\end{lstlisting}

\begin{minipage}{.35\textwidth}
\begin{lstlisting}[
    caption={Output of Z3 for the generated SMT in Listing~\ref{lst:nfa}.},
    label={lst:nfaZ3},basicstyle=\scriptsize,language=lisp
]
sat
s6_3 -> 5
s6_2 -> 1
...

s0_0 -> 4
q7 -> 7
q6 -> 6
...
q0 -> 0
trans -> {
  0 0 -> 4
  4 0 -> 5
...
  3 0 -> (- 5921)
  (- 1) 0 -> (- 8946)
...
  else -> 5
}
final -> {
  2 -> true
  5 -> true
...
  1 -> false
...
  (- 1324) -> false
  else -> false
}
\end{lstlisting}
\end{minipage}
\hfill
\begin{minipage}{.55\textwidth}
\begin{figure}[H]
\centering
\begin{tikzpicture}[>=latex,line join=bevel,scale=.6]
%%
\node (q1) at (349.84bp,107.75bp) [draw,circle] {q1};
  \node (q0) at (63.348bp,142.75bp) [draw,circle] {q0};
  \node (q3) at (250.34bp,26.748bp) [draw,circle, double] {q3};
  \node (q2) at (349.84bp,192.75bp) [draw,circle, double] {q2};
  \node (q5) at (449.33bp,192.75bp) [draw,circle, double] {q5};
  \node (q4) at (154.84bp,196.75bp) [draw,circle] {q4};
  \node (q7) at (250.34bp,196.75bp) [draw,circle] {q7};
  \node (q6) at (154.84bp,111.75bp) [draw,circle] {q6};
  \node (qi) at (1.8bp,142.75bp) [draw,circle, fill] {};
  \draw [->] (q4) ..controls (187.8bp,216.1bp) and (206.11bp,224.89bp)  .. (223.59bp,228.75bp) .. controls (289.99bp,243.41bp) and (310.37bp,244.23bp)  .. (376.58bp,228.75bp) .. controls (390.8bp,225.42bp) and (405.42bp,218.89bp)  .. (q5);
  \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
  \pgfsetstrokecolor{strokecol}
  \draw (300.09bp,247.25bp) node {a};
  \draw [->] (q6) ..controls (183.11bp,118.1bp) and (189.56bp,119.16bp)  .. (195.59bp,119.75bp) .. controls (220.94bp,122.21bp) and (121.7bp,141.89bp)  .. (305.09bp,118.75bp) .. controls (309.28bp,118.22bp) and (313.66bp,117.44bp)  .. (q1);
  \draw (250.34bp,136.25bp) node {a};
  \draw [->] (q3) ..controls (283.88bp,45.478bp) and (295.45bp,52.911bp)  .. (305.09bp,60.748bp) .. controls (313.05bp,67.222bp) and (321.01bp,75.037bp)  .. (q1);
  \draw (300.09bp,68.248bp) node {b};
  \draw [->] (q4) ..controls (189.69bp,196.75bp) and (204.15bp,196.75bp)  .. (q7);
  \draw (200.59bp,204.25bp) node {b};
  \draw [->] (q0) ..controls (96.456bp,131.53bp) and (110.68bp,126.71bp)  .. (q6);
  \draw (109.1bp,136.25bp) node {b};
  \draw [->] (q1) ..controls (301.72bp,103.92bp) and (259.71bp,101.65bp)  .. (223.59bp,103.75bp) .. controls (211.74bp,104.44bp) and (198.81bp,105.78bp)  .. (q6);
  \draw (250.34bp,111.25bp) node {b};
  \draw [->] (q7) ..controls (285.1bp,195.35bp) and (299.58bp,194.77bp)  .. (q2);
  \draw (300.09bp,203.25bp) node {a};
  \draw [->] (q0) ..controls (95.791bp,161.9bp) and (112.28bp,171.63bp)  .. (q4);
  \draw (109.1bp,179.25bp) node {a};
  \draw [->] (q1) ..controls (382.04bp,135.26bp) and (403.75bp,153.81bp)  .. (q5);
  \draw (399.58bp,161.25bp) node {a};
  \draw [->] (qi) ..controls (8.2235bp,142.75bp) and (19.002bp,142.75bp)  .. (q0);
  \draw [->] (q2) ..controls (387.71bp,192.75bp) and (400.54bp,192.75bp)  .. (q5);
  \draw (399.58bp,200.25bp) node {b};
  \draw [->] (q6) ..controls (175.2bp,82.337bp) and (185.08bp,70.08bp)  .. (195.59bp,60.748bp) .. controls (202.27bp,54.82bp) and (210.1bp,49.285bp)  .. (q3);
  \draw (200.59bp,68.248bp) node {b};
%
\end{tikzpicture}
\caption{\label{fig:nfa}Resulting NFA for $m=8$.}
\end{figure}
\end{minipage}

\section*{Problem: mathematical proofs}
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)}
We want to prove that
\begin{enumerate}
  \item \label{itm:logic_a_1} $\forall p \forall q : a(p, a(q, a(p, a(q, a(p, a(q, p)))))) = a(p, q)$
\end{enumerate}
Using the assumptions
\begin{enumerate}[resume]
  \item \label{itm:logic_a_2} $a(x, x) = x$
  \item \label{itm:logic_a_3} $a(x, y) = a(y, x)$
  \item \label{itm:logic_a_4} $a(x, a(y, z)) = a(a(x, y), z)$
\end{enumerate}
We do this by finding a counterexample
\begin{enumerate}[resume]
  \item \label{itm:logic_a_5} $\exists c1, c2 : a(c1, a(c2, a(c1, a(c2, a(c1, a(c2, c1)))))) \neq a(c1, c2)$
\end{enumerate}
First, apply \ref{itm:logic_a_3} to \ref{itm:logic_a_5}
\begin{enumerate}[resume]
  \item \label{itm:logic_a_6} $\exists c1, c2 : a(c1, a(c2, a(c1, a(c2, a(c1, a(c1, c2)))))) \neq a(c1, c2)$
\end{enumerate}
Then, apply \ref{itm:logic_a_2} to \ref{itm:logic_a_4}, where $x \gets x, y \gets x, z \gets y$
\begin{enumerate}[resume]
  \item \label{itm:logic_a_7} $a(x, a(x, y)) = a(x, y)$
\end{enumerate}
On \ref{itm:logic_a_7}, we can then apply \ref{itm:logic_a_3} twice
\begin{enumerate}[resume]
  \item \label{itm:logic_a_8} $a(x, a(y, x)) = a(y, x)$
\end{enumerate}
Finally, we can recursively apply \ref{itm:logic_a_3}, \ref{itm:logic_a_7} and \ref{itm:logic_a_8} to \ref{itm:logic_a_6}, where $c1 \gets x$ and $c2 \gets y$
\begin{enumerate}[resume]
  \item \label{itm:logic_a_9} $a(x, a(y, a(x, a(y, a(x, a(y, x)))))) \neq a(x, a(y, a(x, a(y, a(x, a(y, x))))))$
\end{enumerate}
which evaluates to $FALSE$.\\
Therefore, we found that no counterexample exists, which proves that $a(p, a(q, a(p, a(q, a(p, a(q, p))))))$ indeed rewrites to $a(p, q)$.
\\
We derived this proof with \textit{prover9}, using the following input:
\begin{lstlisting}
formulas(sos).
	a(x,x)=x.
	a(x,y)=a(y,x).
	a(x,a(y,z))=a(a(x,y),z).
end_of_list.

formulas(goals).
	all p all q (a(p,a(q,a(p,a(q,a(p,a(q,p))))))=a(p,q)).
end_of_list.
\end{lstlisting}

\subsubsection*{(b)}
We want to prove 4 things:
\begin{enumerate}
  \item \label{itm:logic_b_1} $\forall x : I * x = x$
  \item \label{itm:logic_b_2} $\forall x : inv(inv(x)) = x$
  \item \label{itm:logic_b_3} $\forall x : inv(x) * x = I$
  \item \label{itm:logic_b_4} $\forall x \forall y : x * y = y * x$
\end{enumerate}
Using the assumptions
\begin{enumerate}[resume]
 \item \label{itm:logic_b_5} $x * (y * z) = (x * y) * z$
 \item \label{itm:logic_b_6} $x * I = x$
 \item \label{itm:logic_b_7} $x * inv(x) = I$
\end{enumerate}

To prove \ref{itm:logic_b_1}, \ref{itm:logic_b_2}, \ref{itm:logic_b_3} and \ref{itm:logic_b_4}, we created the following input:
\begin{lstlisting}
formulas(sos).
	(x*(y*z)=(x*y)*z).
	(x*I=x).
	(x*inv(x)=I).
end_of_list.

formulas(goals).
	all x (I*x=x).
	all x (inv(inv(x))=x).
	all x (inv(x)*x=I).
	all x all y (x*y=y*x).
end_of_list.
\end{lstlisting}

Running this input through \textit{prover9} generated the following proofs for \ref{itm:logic_b_1}, \ref{itm:logic_b_2} and \ref{itm:logic_b_3} respectively:
\begin{lstlisting}[caption=Proof for \ref{itm:logic_b_1}]
1 (all x I * x = x) # label(non_clause) # label(goal).  [goal].
5 x * (y * z) = (x * y) * z.  [assumption].
6 (x * y) * z = x * (y * z).  [copy(5),flip(a)].
7 x * I = x.  [assumption].
8 x * inv(x) = I.  [assumption].
9 I * c1 != c1.  [deny(1)].
13 x * (I * y) = x * y.  [para(7(a,1),6(a,1,1)),flip(a)].
14 x * (inv(x) * y) = I * y.  [para(8(a,1),6(a,1,1)),flip(a)].
19 I * inv(inv(x)) = x.  [para(8(a,1),14(a,1,2)),rewrite([7(2)]),flip(a)].
21 x * inv(inv(y)) = x * y.  [para(19(a,1),6(a,2,2)),rewrite([7(2)])].
22 I * x = x.  [para(19(a,1),13(a,2)),rewrite([21(5),13(4)])].
23 $F.  [resolve(22,a,9,a)].
\end{lstlisting}

\begin{lstlisting}[caption=Proof for \ref{itm:logic_b_2}]
2 (all x inv(inv(x)) = x) # label(non_clause) # label(goal).  [goal].
5 x * (y * z) = (x * y) * z.  [assumption].
6 (x * y) * z = x * (y * z).  [copy(5),flip(a)].
7 x * I = x.  [assumption].
8 x * inv(x) = I.  [assumption].
10 inv(inv(c2)) != c2.  [deny(2)].
13 x * (I * y) = x * y.  [para(7(a,1),6(a,1,1)),flip(a)].
14 x * (inv(x) * y) = I * y.  [para(8(a,1),6(a,1,1)),flip(a)].
19 I * inv(inv(x)) = x.  [para(8(a,1),14(a,1,2)),rewrite([7(2)]),flip(a)].
21 x * inv(inv(y)) = x * y.  [para(19(a,1),6(a,2,2)),rewrite([7(2)])].
22 I * x = x.  [para(19(a,1),13(a,2)),rewrite([21(5),13(4)])].
26 x * (inv(x) * y) = y.  [back_rewrite(14),rewrite([22(5)])].
30 inv(inv(x)) = x.  [para(8(a,1),26(a,1,2)),rewrite([7(2)]),flip(a)].
31 $F.  [resolve(30,a,10,a)].
\end{lstlisting}

\begin{lstlisting}[caption=Proof for \ref{itm:logic_b_3}]
3 (all x inv(x) * x = I) # label(non_clause) # label(goal).  [goal].
5 x * (y * z) = (x * y) * z.  [assumption].
6 (x * y) * z = x * (y * z).  [copy(5),flip(a)].
7 x * I = x.  [assumption].
8 x * inv(x) = I.  [assumption].
11 inv(c3) * c3 != I.  [deny(3)].
13 x * (I * y) = x * y.  [para(7(a,1),6(a,1,1)),flip(a)].
14 x * (inv(x) * y) = I * y.  [para(8(a,1),6(a,1,1)),flip(a)].
19 I * inv(inv(x)) = x.  [para(8(a,1),14(a,1,2)),rewrite([7(2)]),flip(a)].
21 x * inv(inv(y)) = x * y.  [para(19(a,1),6(a,2,2)),rewrite([7(2)])].
22 I * x = x.  [para(19(a,1),13(a,2)),rewrite([21(5),13(4)])].
26 x * (inv(x) * y) = y.  [back_rewrite(14),rewrite([22(5)])].
30 inv(inv(x)) = x.  [para(8(a,1),26(a,1,2)),rewrite([7(2)]),flip(a)].
34 inv(x) * x = I.  [para(30(a,1),8(a,1,2))].
35 $F.  [resolve(34,a,11,a)].
\end{lstlisting}

\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{lstlisting}
formulas(sos).
	(x*(y*z)=(x*y)*z).
	(x*I=x).
	(x*inv(x)=I).
end_of_list.

formulas(goals).
	all x all y (x*y=y*x).
end_of_list.
\end{lstlisting}
After running this input through \textit{mace4}, we retrieved the following finite group $G(I, *, inv)$:
\begin{verbatim}
 I: 0
 
 *:    | 0 1 2 3 4 5
     --*-------------
     0 | 0 1 2 3 4 5 
     1 | 1 0 3 2 5 4
     2 | 2 4 0 5 1 3
     3 | 3 5 1 4 0 2
     4 | 4 2 5 0 3 1
     5 | 5 3 4 1 2 0
 
 inv: 0 -> 0 
      1 -> 1
      2 -> 2
      3 -> 3
      4 -> 4
      5 -> 5
\end{verbatim}
We specify the row number in the $*$-operator table to be the left element, and the column number to be the right element.
Let $x \gets 2$ and $y \gets 1$. Then, we know that $x * y = 2 * 1 = 4$. Also, $y * x = 1 * 2 = 3$. Since $4 \neq 3$, we know that $x * y \neq y * x$, which proves that the property $x * y = y * x$ indeed does not hold for this group.

\if0
\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:}
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:}
\fi


\end{document}