update with dynamic solution for problem 1

[ar1516.git] / ar.tex

diff --git a/ar.tex b/ar.tex
index 94e25f9..b79c70c 100644 (file)
--- a/ar.tex
+++ b/ar.tex
@@ -3,6 +3,23 @@
 \maketitle
 \tableofcontents
 
+\section{Introduction}
+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}.
+
+\begin{lstlisting}[caption={Benchmark system},label={listing:benchmark}]
+CPU: 3600MHz AMD FX(tm)-4100 Quad-Core Processor
+RAM: 8GB
+
+Yices: 2.4.1
+SMT-Lib: 1.2
+Bash: 4.3.30(1)
+\end{lstlisting}
+
 \newpage
 \input{1.tex}