1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
\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{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}
\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}
|
