$i-1$. The crucial part is the location we were in iteration $i-1$ and we make
a disjunction over all possible cities and describe the result in the following
formula called $trans$. We introduce a function $conn(s)$ that returns the set
-of all cities connected to city $s$. $(2)$ deals with the fact that the truck
-can not dump any food in city $S$ and constraints the amount of food dumped in
-the city. $(3)$ deals with the fact that the dumped food is added to the
-current stock of the city. Sub formula $(4)$ deals with the fact that if the
-truck is in $S$ it is replenished and otherwise the dumped load is subtracted
-from the trucks load. Finally $(5)$ deals with the other cities which will have
-their stock decremented with the distance traveled.
+of all cities connected to city $s$. To begin with $(1)$ sets the location of
+the previous iteration correct and checks whether the city will not run out of
+food while travelled too. $(2)$ deals with the fact that the truck can not dump
+any food in city $S$ and constraints the amount of food dumped in the city.
+$(3)$ deals with the fact that the dumped food is added to the current stock of
+the city. Sub formula $(4)$ deals with the fact that if the truck is in $S$ it
+is replenished and otherwise the dumped load is subtracted from the trucks
+load. Finally $(5)$ deals with the other cities which will have their stock
+decremented with the distance traveled.
\begin{align}
\bigvee_{k\in\{S\}\cup V}
l_{i-1}=k\wedge
- \bigvee_{k'\in conn(k)} & l_i=k'\wedge\\
+ \bigvee_{k'\in conn(k)} & l_i=k'\wedge k'_{i-1}\geq dist(k,k')\wedge\\
& (k'=S\wedge d_i=0)\vee(d_i\leq dist(k,k')+k'_{\max}-k'_{i-1}\wedge\\
& (k'\neq S\rightarrow k_i=k_i-dist(k,k')+d_i))\wedge\\
& (k'=S\wedge t_i=t_{\max})\vee t_i=t_{i-1}-d_i\wedge\\
\item \emph{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.}
- Incrementally increasing the number of iterations does not result in a
- state where a city is without food. Therefore we try to find proof that
- the truck is actually capable of keeping all cities saturated.
-
+ Incrementally increasing the number of iterations does result in
+ finding an unsatisfiable formula with $I=21$. Thus there is no infinite
+ path that keeps the cities saturated forever.
+ \item \emph{Show that this is possible if the capacity of the truck is
+ increased to 320 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.)}
To show this we need to prove that there is a state in the state space
that is exactly the same as some previous state. To do this we add the
following formula to the conjunction.
$$
When we incrementally increase the number of iterations we see that
- when we have more then $8$ iterations we encounter a cycle. This is
- shown in the following table where iteration $2$ and iteration $9$ are
- equal. The amount dumped is only shown for more readability. For state
- isomorphism it is not a factor.
+ when we have more then $10$ iterations we encounter a cycle. This is
+ shown in Table~\ref{tbl:s3b} where iteration $4$ and iteration $11$ are
+ equal.
\begin{table}[H]
\centering
\begin{tabular}{lrrrrcr}
\toprule
$I$ & $A$ & $B$ & $C$ & Truck & Location & Dump\\
\midrule
- $0$ & $40$ & $30$ & $145$ & $300$ & $S$ & $0$\\
- $1$ & $19$ & $36$ & $124$ & $273$ & $B$ & $27$\\
- \textbf{2} & \textbf{120} & \textbf{19} & \textbf{107} &
- \textbf{155} & \textbf{A} & \textbf{118}\\
- $3$ & $103$ & $117$ & $90$ & $40$ & $B$ & $115$\\
- $4$ & $82$ & $96$ & $69$ & $300$ & $S$ & $0$\\
- $5$ & $94$ & $67$ & $40$ & $259$ & $A$ & $41$\\
- $6$ & $62$ & $35$ & $194$ & $73$ & $C$ & $186$\\
- $7$ & $25$ & $69$ & $157$ & $2$ & $B$ & $71$\\
- $8$ & $4$ & $48$ & $136$ & $300$ & $S$ & $0$\\
- \textbf{9} & \textbf{120} & \textbf{19} & \textbf{107} &
- \textbf{155} & \textbf{A} & \textbf{145}\\
+ $0$ & $40$ & $30$ & $145$ & $320$ & $S$ & $0$\\
+ $1$ & $19$ & $35$ & $124$ & $294$ & $B$ & $26$\\
+ $2$ & $120$ & $18$ & $107$ & $176$ & $A$ & $118$\\
+ $3$ & $103$ & $120$ & $90$ & $57$ & $B$ & $119$\\
+ \textbf{4} & \textbf{82} & \textbf{99} & \textbf{69} &
+ \textbf{320} & \textbf{S} & \textbf{0}\\
+ $5$ & $119$ & $70$ & $40$ & $254$ & $A$ & $66$\\
+ $6$ & $87$ & $38$ & $194$ & $68$ & $C$ & $186$\\
+ $7$ & $50$ & $67$ & $157$ & $2$ & $B$ & $66$\\
+ $8$ & $29$ & $46$ & $136$ & $320$ & $S$ & $0$\\
+ $9$ & $120$ & $17$ & $107$ & $200$ & $A$ & $120$\\
+ $10$ & $103$ & $120$ & $90$ & $80$ & $B$ & $120$\\
+ \textbf{11} & \textbf{82} & \textbf{99} & \textbf{69} &
+ \textbf{320} & \textbf{S} & \textbf{0}\\
\bottomrule
\end{tabular}
+ \caption{Solution for problem $3b$}\label{tbl:s3b}
\end{table}
- \item \emph{Show that this is possible if the capacity of the truck is
- increased to 320 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.)}
- Solution idem to $(a)$. Just imagine the truck operator glueing $20$
- food packages to the truck which he can not deliver.
\item \emph{Figure out whether it is possible if the capacity of the truck
is set to $318$.}
- Solution idem to $(a)$. Just imagine the truck operator glueing $18$
- food packages to the truck which he can not deliver.
+
\end{enumerate}
(= l$((i-1)) 0)
(or
(and ; now in A
+ (>= a$((i-1)) 29)
(= l$i 1)
(<= d$i (+ 29 (- $AMAX a$((i-1)))))
(= a$i (+ (- a$((i-1)) 29) d$i))
(= t$i (- t$((i-1)) d$i))
) (and ; now in B
+ (>= b$((i-1)) 21)
(= l$i 2)
(<= d$i (+ 21 (- $BMAX b$((i-1)))))
(= b$i (+ (- b$((i-1)) 21) d$i))
(= t$i $TMAX)
) (and ; now in B
+ (>= b$((i-1)) 17)
(= l$i 2)
(<= d$i (+ 17 (- $BMAX b$((i-1)))))
(= b$i (+ (- b$((i-1)) 17) d$i))
(= t$i (- t$((i-1)) d$i))
) (and ; now in C
+ (>= c$((i-1)) 32)
(= l$i 3)
(<= d$i (+ 32 (- $CMAX c$((i-1)))))
(= t$i $TMAX)
) (and ; now in A
+ (>= a$((i-1)) 17)
(= l$i 1)
(<= d$i (+ 17 (- $AMAX a$((i-1)))))
(= a$i (+ (- a$((i-1)) 17) d$i))
(= t$i (- t$((i-1)) d$i))
) (and ; now in C
+ (>= c$((i-1)) 37)
(= l$i 3)
(<= d$i (+ 37 (- $CMAX c$((i-1)))))
(= c$i (+ (- c$((i-1)) 37) d$i))
(= l$((i-1)) 3)
(or
(and ; now in A
+ (>= a$((i-1)) 32)
(= l$i 1)
(<= d$i (+ 32 (- $AMAX a$((i-1)))))
(= a$i (+ (- a$((i-1)) 32) d$i))
(= t$i (- t$((i-1)) d$i))
) (and ; now in B
+ (>= b$((i-1)) 37)
(= l$i 2)
(<= d$i (+ 37 (- $BMAX b$((i-1)))))
(= b$i (+ (- b$((i-1)) 37) d$i))
)
GEN
done
- echo "(or"
- for i in $(seq 0 $ITERATIONS); do
- for j in $(seq $((i+1)) $ITERATIONS); do
- echo "(and (= t$i t$j) (= l$i l$j) (= a$i a$j) (= b$i b$j) (= c$i c$j))"
- done
- done
- echo ")))"
+ echo "))"
}
it=1
-while generate $it 300 | $YICES -m | pee sort "grep -q unsat"
+while generate $it 300 | $YICES | pee sort "grep -q \"^sat\""
do
echo $((it++))
done
(> a$i 0)
(> b$i 0)
(> c$i 0)
+ (>= d$i 0)
+ (<= d$i $TMAX)
+ (>= t$i 0)
+ (<= t$i $TMAX)
(or ;-- ITERATION $i
- (and ;-- SPECIAL CASE FOR STATE S(0)
- (= l$i 0)
- (= d$i 0)
- (= t$i $TMAX)
+ (and ;-- WAS IN S
+ (= l$((i-1)) 0)
(or
- (and ;-- CAME FROM A
- (= l$((i-1)) 1)
- (= a$i (- a$((i-1)) 29))
+ (and ; now in A
+ (>= a$((i-1)) 29)
+ (= l$i 1)
+ (<= d$i (+ 29 (- $AMAX a$((i-1)))))
+ (= a$i (+ (- a$((i-1)) 29) d$i))
+
(= b$i (- b$((i-1)) 29))
(= c$i (- c$((i-1)) 29))
- )
- (and ;-- CAME FROM B
- (= l$((i-1)) 2)
+
+ (= t$i (- t$((i-1)) d$i))
+ ) (and ; now in B
+ (>= b$((i-1)) 21)
+ (= l$i 2)
+ (<= d$i (+ 21 (- $BMAX b$((i-1)))))
+ (= b$i (+ (- b$((i-1)) 21) d$i))
+
(= a$i (- a$((i-1)) 21))
- (= b$i (- b$((i-1)) 21))
(= c$i (- c$((i-1)) 21))
+
+ (= t$i (- t$((i-1)) d$i))
)
)
)
- (and ;-- CASE FOR STATE A(1)
- (= l$i 1)
- (>= d$i 0) (<= d$i t$((i-1))) (<= d$i (- $AMAX a$((i-1))))
- (= t$i (- t$((i-1)) d$i)) (= a$i (+ a$((i-1)) d$i))
-
+ (and ;-- WAS IN A
+ (= l$((i-1)) 1)
(or
- (and ;-- CAME FROM S(0)
- (= l$((i-1)) 0)
+ (and ; now in S
+ (= l$i 0)
+ (= d$i 0)
+
+ (= a$i (- a$((i-1)) 29))
(= b$i (- b$((i-1)) 29))
- (= c$i (- c$((i-1)) 29))
- ) (and ;-- CAME FROM B(2)
- (= l$((i-1)) 2)
- (= b$i (- b$((i-1)) 17))
+ (= c$i (- c$((i-1)) 29))
+
+ (= t$i $TMAX)
+ ) (and ; now in B
+ (>= b$((i-1)) 17)
+ (= l$i 2)
+ (<= d$i (+ 17 (- $BMAX b$((i-1)))))
+ (= b$i (+ (- b$((i-1)) 17) d$i))
+
+ (= a$i (- a$((i-1)) 17))
(= c$i (- c$((i-1)) 17))
- ) (and ;-- CAME FROM C(3)
- (= l$((i-1)) 3)
+
+ (= t$i (- t$((i-1)) d$i))
+ ) (and ; now in C
+ (>= c$((i-1)) 32)
+ (= l$i 3)
+
+ (<= d$i (+ 32 (- $CMAX c$((i-1)))))
+ (= c$i (+ (- c$((i-1)) 32) d$i))
+
+ (= a$i (- a$((i-1)) 32))
(= b$i (- b$((i-1)) 32))
- (= c$i (- c$((i-1)) 32))
+
+ (= t$i (- t$((i-1)) d$i))
)
)
)
- (and ;-- CASE FOR STATE B(2)
- (= l$i 2)
- (>= d$i 0) (<= d$i t$((i-1))) (<= d$i (- $BMAX b$((i-1))))
- (= t$i (- t$((i-1)) d$i)) (= b$i (+ b$((i-1)) d$i))
-
+ (and ;-- WAS IN B
+ (= l$((i-1)) 2)
(or
- (and ;-- CAME FROM S(0)
- (= l$((i-1)) 0)
+ (and ; now in S
+ (= l$i 0)
+ (= d$i 0)
+
(= a$i (- a$((i-1)) 21))
- (= c$i (- c$((i-1)) 21))
- ) (and ;-- CAME FROM A(1)
- (= l$((i-1)) 1)
- (= a$i (- a$((i-1)) 17))
+ (= b$i (- b$((i-1)) 21))
+ (= c$i (- c$((i-1)) 21))
+
+ (= t$i $TMAX)
+ ) (and ; now in A
+ (>= a$((i-1)) 17)
+ (= l$i 1)
+ (<= d$i (+ 17 (- $AMAX a$((i-1)))))
+ (= a$i (+ (- a$((i-1)) 17) d$i))
+
+ (= b$i (- b$((i-1)) 17))
(= c$i (- c$((i-1)) 17))
- ) (and ;-- CAME FROM C(3)
- (= l$((i-1)) 3)
+
+ (= t$i (- t$((i-1)) d$i))
+ ) (and ; now in C
+ (>= c$((i-1)) 37)
+ (= l$i 3)
+ (<= d$i (+ 37 (- $CMAX c$((i-1)))))
+ (= c$i (+ (- c$((i-1)) 37) d$i))
+
(= a$i (- a$((i-1)) 37))
- (= c$i (- c$((i-1)) 37))
+ (= b$i (- b$((i-1)) 37))
+
+ (= t$i (- t$((i-1)) d$i))
)
)
)
- (and ;-- CASE FOR STATE C(3)
- (= l$i 3)
- (>= d$i 0) (<= d$i t$((i-1))) (<= d$i (- $CMAX c$((i-1))))
- (= t$i (- t$((i-1)) d$i)) (= c$i (+ c$((i-1)) d$i))
-
+ (and ;-- WAS IN C
+ (= l$((i-1)) 3)
(or
- (and ;-- CAME FROM A(1)
- (= l$((i-1)) 1)
- (= a$i (- a$((i-1)) 32))
+ (and ; now in A
+ (>= a$((i-1)) 32)
+ (= l$i 1)
+ (<= d$i (+ 32 (- $AMAX a$((i-1)))))
+ (= a$i (+ (- a$((i-1)) 32) d$i))
+
(= b$i (- b$((i-1)) 32))
- ) (and ;-- CAME FROM B(2)
- (= l$((i-1)) 2)
+ (= c$i (- c$((i-1)) 32))
+
+ (= t$i (- t$((i-1)) d$i))
+ ) (and ; now in B
+ (>= b$((i-1)) 37)
+ (= l$i 2)
+ (<= d$i (+ 37 (- $BMAX b$((i-1)))))
+ (= b$i (+ (- b$((i-1)) 37) d$i))
+
(= a$i (- a$((i-1)) 37))
- (= b$i (- b$((i-1)) 37))
+ (= c$i (- c$((i-1)) 37))
+
+ (= t$i (- t$((i-1)) d$i))
)
)
)
done
echo ")))"
}
-
it=1
-while generate $it 320 | $YICES -m | pee sort "grep unsat"
+while generate $it 320 | $YICES -m | pee sort "grep -q unsat"
do
- it=$((it+1))
+ echo $((it++))
done
-echo $it
--- /dev/null
+#!/bin/bash
+YICES=~/projects/yices-2.4.2/bin/yices-smt
+AI=40
+BI=30
+CI=145
+AMAX=120
+BMAX=120
+CMAX=200
+
+function generate {
+ ITERATIONS=$1
+ TMAX=$2
+ cat<<GEN
+(benchmark a1.smt
+:logic QF_UFLIA
+:extrafuns (
+$( for i in $(seq 0 $ITERATIONS); do
+ echo -e "\t(a$i Int) (b$i Int) (c$i Int) (t$i Int) (l$i Int) (d$i Int)"
+ done)
+)
+:formula
+(and
+ ;-- PRECONDITION
+ (and (= a0 $AI) (= b0 $BI) (= c0 $CI) (= t0 $TMAX) (= l0 0) (= d0 0))
+GEN
+ for i in $(seq 1 $ITERATIONS); do
+ cat<<GEN
+ (> a$i 0)
+ (> b$i 0)
+ (> c$i 0)
+ (>= d$i 0)
+ (<= d$i $TMAX)
+ (>= t$i 0)
+ (<= t$i $TMAX)
+ (or ;-- ITERATION $i
+ (and ;-- WAS IN S
+ (= l$((i-1)) 0)
+ (or
+ (and ; now in A
+ (>= a$((i-1)) 29)
+ (= l$i 1)
+ (<= d$i (+ 29 (- $AMAX a$((i-1)))))
+ (= a$i (+ (- a$((i-1)) 29) d$i))
+
+ (= b$i (- b$((i-1)) 29))
+ (= c$i (- c$((i-1)) 29))
+
+ (= t$i (- t$((i-1)) d$i))
+ ) (and ; now in B
+ (>= b$((i-1)) 21)
+ (= l$i 2)
+ (<= d$i (+ 21 (- $BMAX b$((i-1)))))
+ (= b$i (+ (- b$((i-1)) 21) d$i))
+
+ (= a$i (- a$((i-1)) 21))
+ (= c$i (- c$((i-1)) 21))
+
+ (= t$i (- t$((i-1)) d$i))
+ )
+ )
+ )
+ (and ;-- WAS IN A
+ (= l$((i-1)) 1)
+ (or
+ (and ; now in S
+ (= l$i 0)
+ (= d$i 0)
+
+ (= a$i (- a$((i-1)) 29))
+ (= b$i (- b$((i-1)) 29))
+ (= c$i (- c$((i-1)) 29))
+
+ (= t$i $TMAX)
+ ) (and ; now in B
+ (>= b$((i-1)) 17)
+ (= l$i 2)
+ (<= d$i (+ 17 (- $BMAX b$((i-1)))))
+ (= b$i (+ (- b$((i-1)) 17) d$i))
+
+ (= a$i (- a$((i-1)) 17))
+ (= c$i (- c$((i-1)) 17))
+
+ (= t$i (- t$((i-1)) d$i))
+ ) (and ; now in C
+ (>= c$((i-1)) 32)
+ (= l$i 3)
+
+ (<= d$i (+ 32 (- $CMAX c$((i-1)))))
+ (= c$i (+ (- c$((i-1)) 32) d$i))
+
+ (= a$i (- a$((i-1)) 32))
+ (= b$i (- b$((i-1)) 32))
+
+ (= t$i (- t$((i-1)) d$i))
+ )
+ )
+ )
+ (and ;-- WAS IN B
+ (= l$((i-1)) 2)
+ (or
+ (and ; now in S
+ (= l$i 0)
+ (= d$i 0)
+
+ (= a$i (- a$((i-1)) 21))
+ (= b$i (- b$((i-1)) 21))
+ (= c$i (- c$((i-1)) 21))
+
+ (= t$i $TMAX)
+ ) (and ; now in A
+ (>= a$((i-1)) 17)
+ (= l$i 1)
+ (<= d$i (+ 17 (- $AMAX a$((i-1)))))
+ (= a$i (+ (- a$((i-1)) 17) d$i))
+
+ (= b$i (- b$((i-1)) 17))
+ (= c$i (- c$((i-1)) 17))
+
+ (= t$i (- t$((i-1)) d$i))
+ ) (and ; now in C
+ (>= c$((i-1)) 37)
+ (= l$i 3)
+ (<= d$i (+ 37 (- $CMAX c$((i-1)))))
+ (= c$i (+ (- c$((i-1)) 37) d$i))
+
+ (= a$i (- a$((i-1)) 37))
+ (= b$i (- b$((i-1)) 37))
+
+ (= t$i (- t$((i-1)) d$i))
+ )
+ )
+ )
+ (and ;-- WAS IN C
+ (= l$((i-1)) 3)
+ (or
+ (and ; now in A
+ (>= a$((i-1)) 32)
+ (= l$i 1)
+ (<= d$i (+ 32 (- $AMAX a$((i-1)))))
+ (= a$i (+ (- a$((i-1)) 32) d$i))
+
+ (= b$i (- b$((i-1)) 32))
+ (= c$i (- c$((i-1)) 32))
+
+ (= t$i (- t$((i-1)) d$i))
+ ) (and ; now in B
+ (>= b$((i-1)) 37)
+ (= l$i 2)
+ (<= d$i (+ 37 (- $BMAX b$((i-1)))))
+ (= b$i (+ (- b$((i-1)) 37) d$i))
+
+ (= a$i (- a$((i-1)) 37))
+ (= c$i (- c$((i-1)) 37))
+
+ (= t$i (- t$((i-1)) d$i))
+ )
+ )
+ )
+ )
+GEN
+ done
+# echo "(or"
+# for i in $(seq 0 $ITERATIONS); do
+# for j in $(seq $((i+1)) $ITERATIONS); do
+# echo "(and (= t$i t$j) (= l$i l$j) (= a$i a$j) (= b$i b$j) (= c$i c$j))"
+# done
+# done
+# echo ")"
+ echo "))"
+}
+it=1
+while generate $it 318 | $YICES | pee sort "grep -q \"^sat\""
+do
+ echo $((it++))
+done
repositories / ar1516.git / commitdiff