incrementing a special variable called \texttt{<REP>} which is an instantiation
of $n(p)$. When the iteration yields unsat we know that the current number
minus one is the maximum amount of prittles the trucks can carry. The
-maximization is done with a bash script shown in Listing~\ref{listing:1.bash}.
+maximization is done with a bash script shown in Listing~\ref{listing:1.bash}
+and visualized with the python script shown in Listing~\ref{listing:a1.py}
\lstinputlisting[language=bash,firstline=66,
caption={Iteratively find the largest solution for problem 1},
\subsection{SMT format solution}
The formula is easily convertable via a Python script to SMT format by literal
-conversion and said script is listed in Listing~\ref{listing:a2.py}. The Python
-script optimizes a little bit from the original formula by leaving out the
-overlap checking between the same components. The solution is calculated using
-the command shown in Listing~\ref{listing:2.bash}
+conversion and said script is listed in Listing~\ref{listing:a2.bash}. The
+Python script optimizes a little bit from the original formula by leaving out
+the overlap checking between the same components. The solution is calculated
+using the command shown in Listing~\ref{listing:2.bash} and visualized with the
+python script shown in Listing~\ref{listing:a2.py}
\lstinputlisting[language=bash,
caption={Find the shortest solution for problem 3},
Finding this solution takes less then $35$ seconds and is shown in
Table~\ref{tab:s2}.
+The bold items represent the power components.
+
\begin{table}[H]
\centering
\input{a2.tex}
script optimizes a little bit from the original formula by leaving out the
shared resource checking for the same jobs. The minimization is done by
incrementing variable $T$ every time the current $T$ yields unsat with a bash
-script shown in Listing~\ref{listing:3.bash}.
+script shown in Listing~\ref{listing:3.bash} and visualized with the python
+script shown in Listing~\ref{listing:a3.py}.
\lstinputlisting[language=bash,firstline=46,
caption={Iteratively find the shortest solution for problem 3},
\subsection{Solution}
The bash script finds and shows the minimal solution in which all jobs are
-finished in $37$ time units. Finding this solution takes less then $0.85$
-seconds and is shown in Figure~\ref{tab:s3}.
+finished in $37$ time units. Finding this solution takes less then $0.42$
+seconds and is shown in Table~\ref{tab:s3}.
+
+The bold items represent the jobs using shared resources.
\begin{table}[H]
\centering
looped over. The script also optimizes by not checking variables $a_0^n$ and
$a_I^n$ since they always stay the same anyways. The minimization is done by
incrementing variable $N$ every time the current $N$ yields unsat with a bash
-script shown in Listing~\ref{listing:4.bash}.
+script shown in Listing~\ref{listing:4.bash} and visualized with the python
+script shown in Listing~\ref{listing:a4.py}.
\lstinputlisting[language=bash,firstline=58,
caption={Iteratively find the shortest solution for problem 4},
\subsection{Solution}
The bash script finds and shows the minimal solution in which the postcondition
-is satisfied for $N=10$. Finding this solution takes less then $75$ seconds and
+is satisfied for $N=10$. Finding this solution takes less then $20$ seconds and
is shown in Table~\ref{tab:s4}.
Every line in the table represents the iteration and the bold items represent
$(LATEX) -ini -jobname="$(basename $@)" "&$(LATEX) $<\dump"
a%.tex: src/a%.bash src src/a%.py
- bash $< $@ >/dev/null
+ bash $< $@
clean:
$(RM) -v $(addprefix $(DOCUMENT).,fmt aux log out toc pdf) $(SOLUTIONS)
-\section{Appendix}
+\section{Appendix}\label{sec:appendix}
\begin{lstlisting}[caption={Benchmark system}]
OS: Linux 3.16.0-4-amd64 #1 SMP Debian 3.16 x86_64 GNU/Linux
CPU: 3600MHz AMD FX(tm)-4100 Quad-Core Processor
\end{lstlisting}
\newpage
-\lstinputlisting[language=lisp,caption={a1.bash},
+\lstinputlisting[language=bash,caption={a1.bash},
label={listing:a1.bash}]{src/a1.bash}
+\lstinputlisting[language=python,caption={a1.py},
+ label={listing:a1.py}]{src/a1.py}
\newpage
+\lstinputlisting[language=bash,caption={a2.bash},
+ label={listing:a2.bash}]{src/a2.bash}
\lstinputlisting[language=python,caption={a2.py},
label={listing:a2.py}]{src/a2.py}
\newpage
-\lstinputlisting[language=python,caption={a3.bash},
- label={listing:a3.py}]{src/a3.bash}
+\lstinputlisting[language=bash,caption={a3.bash},
+ label={listing:a3.bash}]{src/a3.bash}
+\lstinputlisting[language=python,caption={a3.py},
+ label={listing:a3.py}]{src/a3.py}
\newpage
-\lstinputlisting[language=python,caption={a4.bash},
+\lstinputlisting[language=bash,caption={a4.bash},
label={listing:a4.bash}]{src/a4.bash}
+\lstinputlisting[language=python,caption={a4.py},
+ label={listing:a4.py}]{src/a4.py}
\tableofcontents
\setcounter{section}{-1}
-\section{Introduction}
+\section{General approach}
Implementing all the problems by hand in SMT-Lib format would be too much work
-and therefore all problems have an accompanying bash script that does the
-generation and/or the mini or maximization. The bash scripts all have a
-function defined called \lstinline{generate} with a parameter that will be used
-for mini or maximization. All solving is done on the benchmark system listed in
-Listing~\ref{listing:benchmark}.
+and therefore all problems have an accompanying bash script contains a function
+\lstinline{generate} that generates the SMT-Lib format. The script feeds the
+SMT-Lib format to yices after which the output is feeded to a Python script
+that visualizes the solution. This means that for all problems $p$ for $p\in
+\{1,\ldots, 4\}$ there exist $2$ files. \texttt{ap.bash} that generates the
+solution and \texttt{ap.py} that visualizes the solution. Both files are
+present in the Section~\ref{sec:appendix}. All solving is done on the benchmark
+system listed in Listing~\ref{listing:benchmark}.
\begin{lstlisting}[caption={Benchmark system},label={listing:benchmark}]
CPU: 3600MHz AMD FX(tm)-4100 Quad-Core Processor
)
GENERATE
}
-
-i=1
+time { i=1
while [ $(generate $i | yices-smt) = "sat" ]; do
echo "n(p)=$i is still sat"
i=$((i+1))
done
echo "n(p)=$i is unsat thus maximum n(p)=$((i-1))"
+}
generate $((i-1)) | yices-smt -m | python3 src/a1.py > $1
done
echo "))"
}
-generate | yices-smt -m | python3 src/a2.py > $1
+time generate | yices-smt -m | python3 src/a2.py > $1
for line in sys.stdin:
match = re.match('\(= c(?P<c>\d+)(?P<t>.) (?P<v>\d+)\)', line)
if match:
- comps[match.group('c')] = comps.get(match.group('c'), {})
- comps[match.group('c')][match.group('t')] = int(match.group('v'))
+ c = int(match.group('c'))
+ comps[c] = comps.get(c, {})
+ comps[c][match.group('t')] = int(match.group('v'))
maxx = max(c['x']+c['w'] for c in comps.values())
maxy = max(c['y']+c['h'] for c in comps.values())
comps[c]['y'] + comps[c]['h'] >= y and comps[c]['y'] <= y and
comps[c]['x'] + comps[c]['w'] >= x and comps[c]['x'] <= x]
if cs:
- print('\\hspace{{.5mm}}{}\\hspace{{.5mm}}'.format(cs[0]), end='')
+ print('\\hspace{{.5mm}}{}\\hspace{{.5mm}}'.format(
+ '\mathbf{{{}}}'.format(cs[0]) if cs[0] <= 3 else cs[0]), end='')
if x != maxx:
print(' & ', end='')
print('\\\\')
echo "))"
}
-i=1
+time { i=1
while [ $(generate $i | yices-smt) = "unsat" ]; do
echo "T=$((i++)) is still unsat"
done
echo "T=$i is sat thus the minimum T=$i"
+}
generate $i | yices-smt -m | python3 src/a3.py > $1
for t in range(1, tmax):
cj = [j for j in jobs if levels[j] == d and j in schedule[t]]
if cj:
- print('\\hspace{{.5mm}}{}\\hspace{{.5mm}}'.format(cj[0]), end='')
+ print('\\hspace{{.5mm}}{}\\hspace{{.5mm}}'.format(
+ '\\mathbf{{{}}}'.format(cj[0])
+ if cj[0] in [5, 7, 10] else cj[0]), end='')
if t != tmax-1:
print(' & ', end='')
print('\\\\')
echo ")))"
}
-i=1
+time { i=1
while [ $(generate $i | yices-smt) = "unsat" ]; do
echo "N=$i is still unsat"
i=$((i+1))
done
echo "N=$i is sat thus minimum N=$i"
+}
generate $i | yices-smt -m | python src/a4.py > $1
repositories / ar1516.git / commitdiff