path: root/part2.tex

\documentclass[12pt]{article}
\usepackage{a4wide}
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{epic}
\usepackage{graphicx}
\usepackage{gensymb}
\usepackage[table]{xcolor}
\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)}
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 definitions path travelling costs $cost$, the truck and villages
$V$ (and their capacities $capacity$) we are able to build the route that the
truck travels, parameterized under the $m$ (the number of visited locations).
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 would still be \texttt{unsat} (after four seconds)
while for $m=21$ a solution was found within a second. This shows that a valid
route can be obtained where 21 locations are visited, but that no route exists
that passes through 22 locations. 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)
...
(s0_30 Int) (s1_30 Int) ... (s4_30 Int) (l30 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 by the augmented generator 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 (
...
(s0_13 Int) (s1_13 Int) ... (s4_13 Int) (l13 Int)
(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
\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 (truck and village stock and current location
$l_j$) after $j$ transitions. State $j=13$ has higher 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:}


\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}