From: Mart Lubbers <mart@martlubbers.net>
Date: Fri, 23 Oct 2015 07:43:32 +0000 (+0200)
Subject: ar finished
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=5e74751948a4527cdc575ad43169502bdf1be65d;p=master.git

ar finished
---

diff --git a/ar/assignment1/.gitignore b/ar/assignment1/.gitignore
new file mode 100644
index 0000000..2d3a43f
--- /dev/null
+++ b/ar/assignment1/.gitignore
@@ -0,0 +1,7 @@
+ar.log
+ar.fmt
+ar.fmt
+ar.aux
+ar.out
+ar.toc
+ar.pdf
diff --git a/ar/assignment1/1.tex b/ar/assignment1/1.tex
new file mode 100644
index 0000000..098a2e3
--- /dev/null
+++ b/ar/assignment1/1.tex
@@ -0,0 +1,115 @@
+\section{Problem 1}
+{\em
+Six trucks have to deliver pallets of obscure building blocks to a magic
+factory. Every truck has a capacity of 7800 kg and can carry at most
+eight pallets. In total, the following has to be delivered:
+\begin{itemize}
+	\item Four pallets of nuzzles, each of weight 700 kg.
+	\item A number of pallets of prittles, each of weight 800 kg.
+	\item Eight pallets of skipples, each of weight 1000 kg.
+	\item Ten pallets of crottles, each of weight 1500 kg.
+	\item Five pallets of dupples, each of weight 100 kg.
+\end{itemize}
+Prittles and crottles are an explosive combination: they are not allowed to be
+put in the same truck.
+
+Skipples need to be cooled; only two of the six trucks have facility for
+cooling skipples. Dupples are very valuable; to distribute the risk of loss no
+two pallets of dupples may be in the same truck.
+
+Investigate what is the maximum number of pallets of prittles that can be
+delivered, and show how for that number all pallets may be divided over the six
+trucks.
+}
+
+\newpage
+\subsection{Formal definition}
+For every truck $t_i$ for $i\in T$ where $T=\{1,\ldots,6\}$ in combination with
+every nuzzle $n$, prittle $p$, skipple $s$, crottle $c$ and dupple $d$ we
+declare a variable that holds the amount of that type of building block in that
+truck. We group all pallets $r\in P$ where $P=\{n,p,s,c,d\}$. We also
+define function $w(r)$ that defines the weight of the pallet and $n(r)$ that
+defines the number of pallets needed.
+
+This leads to the following formalization where we maximize $n(p)$.
+
+\begin{align}
+	\bigwedge^{T}_{i=1}\Biggl(
+	& \bigwedge_{r\in P}t_{i}r\geq0\\
+	& \wedge \sum_{r\in P}t_{i}r\leq8\\
+	& \wedge \left(\sum_{r\in P}t_{i}r\cdot w(r)\right)\leq7800)\\
+	& \wedge (t_{i}p=0\vee t_{i}c=0)\\
+	& \wedge t_{i}d\leq1\\
+	& \wedge (t_{i}=t_{1} \vee t_{i}=t_{2} \vee t_{i}s=0)\Biggr)\wedge\\
+	\bigwedge_{r\in P}\Biggl(
+	& \left(\sum^{T}_{i=1}t_{i}r\right)=n(r)\Biggr)
+\end{align}
+
+Every numbered subformula describes a constraint from the problem description.
+We can separated the subformulas in formulas going over all trucks and formulas
+going over all pallets.
+
+\begin{itemize}
+	\item \textbf{Trucks}
+	\begin{enumerate}
+		\item Makes sure you can not have a negative number of pallets
+			in a truck by stating that the number of pallets in a
+			truck is not smaller then $0$.
+		\item Makes sure you can not have more then $8$ pallets in a
+			truck by stating that the sum of all pallets in a truck
+			is not bigger then $8$.
+		\item Makes sure the weight will never go over the maximum
+			weight per truck by stating that all the pallets times
+			their weight in a truck will not go over $7800$kg.
+		\item Makes sure prittles and crottles are never together in a
+			truck by stating that either the number of prittles is
+			zero or the number of crottles is zero in a truck.
+		\item Makes sure that skipples are only in the first two cooled
+			trucks by stating that if the truck number not one or
+			two the number of skipples is zero.
+	\end{enumerate}
+	\item \textbf{Pallets}
+	\begin{enumerate}
+		\setcounter{enumi}{6}
+		\item Makes sure that all mandatory pallets are transported by
+			summing over all trucks and assuring the number of the
+			pallets of that type is exactly $n(r)$.
+	\end{enumerate}
+\end{itemize}
+
+\subsection{SMT format solution}
+The formula is easily convertable to SMT format by literal conversion and is
+listed in Listing~\ref{listing:a1.smt}. The maximization is done by
+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}.
+
+\lstinputlisting[language=bash,
+	caption={Iteratively find the largest solution for problem 1},
+	label={listing:1.bash}]{src/a1.bash}
+
+\subsection{Solution}
+The bash script finds and shows the maximal solution of $18$ prittles. Finding
+this solution takes less then $0.12$ seconds and is shown in Table~\ref{tab:s1}.
+
+\begin{table}[H]
+	\centering
+	\begin{tabular}{l|lllll|ll}
+		\toprule
+		Truck & Nuzzles & Prittles & Skipples & Crottles & Dupples &
+			Weight & Pallets\\
+		\midrule
+		1 & 0 & 0 & 4 & 2 & 1 & 7100 & 7\\
+		2 & 0 & 3 & 4 & 0 & 1 & 6500 & 8\\
+		3 & 0 & 8 & 0 & 0 & 0 & 6400 & 7\\
+		4 & 0 & 7 & 0 & 0 & 1 & 5700 & 8\\
+		5 & 0 & 0 & 0 & 5 & 1 & 7600 & 6\\
+		6 & 4 & 0 & 0 & 3 & 1 & 7400 & 8\\
+		\midrule
+		total & 4 & 18 & 8 & 10 & 5 & &\\
+		\bottomrule
+	\end{tabular}
+	\caption{Solution visualization for problem 1}
+\label{tab:s1}
+\end{table}
diff --git a/ar/assignment1/2.tex b/ar/assignment1/2.tex
new file mode 100644
index 0000000..12ed33d
--- /dev/null
+++ b/ar/assignment1/2.tex
@@ -0,0 +1,122 @@
+\section{Problem 2}
+{\em
+ Give a chip design containing three power components and eight regular
+components satisfying the following constraints:
+
+\begin{itemize}
+	\item The width of the chip is 29 and the height is 22.
+	\item All power components have width 4 and height 2.
+	\item The sizes of the eight regular components are $9\times7$,
+		$12\times6,$ $10\times7,$ $18\times5,$ $20\times4,$
+		$10\times6,$ $8\times6$ and $10\times8$ respectively.
+	\item All components may be turned 90, but may not overlap.
+	\item In order to get power, all regular components should directly be
+		connected to a power component, that is, an edge of the
+		component should have at least one point in common with an edge
+		of the power component.
+	\item Due to limits on heat production the power components should be
+		not too close: their centres should differ at least $17$ in
+		either the $x$ direction or the $y$ direction (or both).
+\end{itemize}
+}
+
+\newpage
+\subsection{Formal definition}
+For every component $c_{i}$ for $i\in PC\cup RC$ where $PC=\{1,\ldots,3\}$ and
+$RC=\{4,\ldots,11\}$ we define a width, a height, an $x$ and a $y$ variables
+$c_{i}w$, $c_{i}h$, $c_{i}x$ and $c_{i}y$. $c_ih$ does not necessarily have the
+specified height of the components since the components may be rotated. For the
+specified width and height we introduce the functions $h(c)$ and $w(c)$ that
+return the specified width and height.
+
+This leads to the following formalization.
+
+\begin{align}
+	\bigwedge_{i\in PC\cup RC}\Biggl(
+	  & (c_{i}h=h(i)\vee c_{i}h=w(i))\wedge(c_{i}w=w(i)\vee c_{i}w=h(i))\\
+		& \wedge 29-c_{i}w\geq c_{i}x>0\wedge 22-c_{i}h\geq c_{i}y>0\\
+		& \wedge \bigwedge_{j\in PC\cup RC}\Bigl(j\geq i\\
+		\nonumber & \qquad\qquad\qquad \vee c_{i}x>c_{j}x+c_{j}w\\
+		\nonumber & \qquad\qquad\qquad \vee c_{i}x+c_{j}w<c_{j}x\\
+		\nonumber & \qquad\qquad\qquad \vee c_{i}y>c_{j}y+c_{j}h\\
+		\nonumber & \qquad\qquad\qquad 
+			\vee c_{i}y+c_{j}h<c_{j}h\Bigr)\Biggr)\wedge\\
+	\bigwedge_{i\in PC}\bigwedge_{j\in PC}\Biggl( & i=j\\
+		\nonumber & \vee c_{i}x+\nicefrac{c_{i}w}{2}-
+			c_{j}x+\nicefrac{c_{j}w}{2}>17\\
+		\nonumber & \vee c_{j}x+\nicefrac{c_{j}w}{2}-
+			c_{i}x+\nicefrac{c_{i}w}{2}>17\\
+		\nonumber & \vee c_{i}y+\nicefrac{c_{i}h}{2}-
+			c_{j}y+\nicefrac{c_{j}h}{2}>17\\
+		\nonumber & \vee c_{j}y+\nicefrac{c_{j}h}{2}-
+			c_{i}y+\nicefrac{c_{i}h}{2}>17\Biggr)\wedge\\
+	\bigwedge_{i\in RC}\bigvee_{j\in PC}\neg\Biggl(
+		& (c_{i}x-1>c_{j}x+c_{j}w\\
+		\nonumber & \vee c_{i}x+1+c_{j}w<c_{j}x\\
+		\nonumber & \vee c_{i}y-1>c_{j}y+c_{j}h\\
+		\nonumber & \vee c_{i}y+1+c_{j}h<c_{j}h\Biggr)
+\end{align}
+
+Every numbered subformula describes a constraint from the problem description.
+We can separated the subformulas in formulas going over all components, only
+power components and only regular components.
+\begin{itemize}
+	\item\textbf{All}
+		\begin{enumerate}
+			\setcounter{enumi}{7}
+			\item Makes sure the width and the height of the
+				component can be swapped thus allowing a
+				rotation.
+			\item Makes sure the components are placed on the
+				chip by stating that the $x$ and $y$
+				coordinates are bigger then $0$ and the $x$ and
+				$y$ plus their width or height does not exceed
+				the specified width and height of the chip.
+			\item Makes sure the components do not overlap by
+				defining for all pairs of components that they
+				either are strictly right, strictly left,
+				strictly above or strictly below the other.
+		\end{enumerate}
+	\item\textbf{Power only}
+		\begin{enumerate}
+			\setcounter{enumi}{10}
+			\item Makes sure power components are at least $17$
+				block away from other power components by
+				stating that the difference between the center
+				of each pair of components is bigger then $17$.
+		\end{enumerate}
+	\item\textbf{Regular only}
+		\begin{enumerate}
+			\setcounter{enumi}{11}
+			\item Makes sure regular components are connected to a
+				power component by stating, using the same
+				method as in the overlay, that it has overlap
+				with a power component that has had its size
+				increased by $1$.
+		\end{enumerate}
+\end{itemize}
+
+\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}
+
+\lstinputlisting[language=bash,
+	caption={Find the shortest solution for problem 3},
+	label={listing:2.bash}]{src/a2.bash}
+
+\subsection{Solution}
+Finding this solution takes less then $35$ seconds and is shown in
+Figure~\ref{fig:s2}.
+
+Light gray blocks represent regular components and the darker gray
+blocks represent power components.
+
+\begin{figure}[H]
+	\centering
+	\includegraphics[scale=0.70]{s2.png}
+\label{fig:s2}
+	\caption{Solution visualization for problem 2}
+\end{figure}
diff --git a/ar/assignment1/3.tex b/ar/assignment1/3.tex
new file mode 100644
index 0000000..cf68821
--- /dev/null
+++ b/ar/assignment1/3.tex
@@ -0,0 +1,77 @@
+\section{Problem 2}
+{\em
+Twelve jobs numbered from 1 to 12 have to be executed satisfying the following
+requirements:
+\begin{itemize}
+	\item The running time of job $i$ is $i$, for $i=1,\ldots,12$
+	\item All jobs run without interrupt.
+	\item Job 3 may only start if jobs 1 and 2 have been finished.
+	\item Job 5 may only start if jobs 3 and 4 have been finished.
+	\item Job 7 may only start if jobs 3, 4 and 6 have been finished.
+	\item Job 9 may only start if jobs 5 and 8 have been finished
+	\item Job 11 may only start if job 10 has been finished.
+	\item Job 12 may only start if jobs 9 and 11 have been finished.
+	\item Jobs 5,7 en 10 require a special equipment of which only one copy
+		is available, so no two of these jobs may run at the same time.
+\end{itemize}
+
+Find a solution of this scheduling problem for which the total running time is
+minimal.
+}
+
+\newpage
+\subsection{Formal definition}
+For every job $j_{i}$ for $i\in J$ where $J=\{1,\ldots,12\}$ we define variable
+$j_{i}s$ for starting time. All jobs that have a shared resource we group as
+$J'=\{5,7,10\}$ and we define a function $p(i)$ that returns a set of all
+dependencies of job $i$. The total time it takes for all jobs to finish is $T$.
+
+This leads to the following formalization where we minimize $T$.
+\begin{align}
+	\bigwedge_{i\in J}\Biggl( 
+		& j_{i}>0\wedge j_{i}+i<T\\
+		& \wedge \bigwedge_{k\in p(i)} j_{i}>j_{k}+k\Biggr)\\
+		& \wedge \bigwedge_{i\in J'}\bigwedge_{k\in J'}
+		i=j\vee j_{i}>j_{k}+k \vee j_{i}+i<j_{k}
+\end{align}
+
+Every numbered subformula describes a group of constraints from the problem
+definition.
+\begin{itemize}
+	\setcounter{enumi}{12}
+	\item Makes sure that starting times are positive and that all jobs
+		finish before $T$.
+	\item Makes sure that job may not start before all their dependencies
+		are finished by stating that they start strictly after their
+		dependency.
+	\item Makes sure that never two more jobs use the shared resource by
+		stating that they either ends strictly before the other or
+		start strictly after the other.
+\end{itemize}
+
+\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:a3.py}. The Python
+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}.
+
+\lstinputlisting[language=bash,
+	caption={Iteratively find the shortest solution for problem 3},
+	label={listing:3.bash}]{src/a3.bash}
+
+\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{fig:s3}. 
+
+Light gray blocks represent normal tasks and the darker gray blocks represent
+tasks from $J'$.
+
+\begin{figure}[H]
+	\centering
+	\includegraphics[width=\linewidth]{s3.png}
+\label{fig:s3}
+	\caption{Solution visualization for problem 3}
+\end{figure}
diff --git a/ar/assignment1/4.tex b/ar/assignment1/4.tex
new file mode 100644
index 0000000..153cfec
--- /dev/null
+++ b/ar/assignment1/4.tex
@@ -0,0 +1,89 @@
+\section{Problem 4}
+{\em
+Seven integer variables $a_1; a_2; a_3; a_4; a_5; a_6; a_7$ are given, for
+which the initial value of $a_i$ is $i$ for $i=1,\ldots,I$ where $I=7$. The
+following steps are defined: choose $i$ with $1<i<7$ and execute
+$$a_i:=a_{i-1}+a_{i+1}$$
+that is, $a_i$ gets the sum of the values of its
+neighbors and all other values remain unchanged. Show how it is possible that
+after a number of steps a number of steps a number $\geq 50$ occurs at least
+twice in $a_1; a_2; a_3; a_4; a_5; a_6; a_7$.
+}
+
+\newpage
+\subsection{Formal definition}
+For every variable $a_i$ for $i\in I$ where $I=\{1,\ldots,7\}$ we define
+variables for all iterations $n$ for $n\in N$ where $N=\{1,\ldots,K\}$ for a
+fixed $K$ and call the $a_i^n$.
+
+This leads to the following formalization where we minimize $K$.
+
+\begin{align}
+	\bigwedge_{i\in I}a_i^0=i\wedge\\
+	\bigwedge_{n\in N}\Biggl(\bigvee_{i\in I}\Bigl( 
+		& j\neq 0\wedge j\neq I\wedge
+			a_i^n=a_{i-1}^{n-1}+a_{i+1}^{n-1}\wedge\\
+	\nonumber & \bigwedge_{j\in I}i\neq j\wedge
+			a_j^n=a_j^{n-1}\Bigr)\Biggr)\\
+	\bigvee_{i\in I}\Biggl(
+		& a_i^N\geq50\wedge 
+		\bigvee_{j\in I}i\neq j\wedge a_i^N=a_j^N\Biggr)
+\end{align}
+
+Every number subformula describes either the precondition, program or
+postcondition.
+\begin{enumerate}
+	\setcounter{enumi}{15}
+	\item Makes sure all $a_i^0$ have the specified initial value.
+	\item Makes sure that in one iteration zero or one of the $a_i$ becomes
+		the sum of its neighbors by stating in the first part that
+		$a_i^n=a_{i-1}^{n-1}+a_{i+1}^{n-1}$ for $i$ not being $0$ or
+		$I$. The second part states that all other $a_i$ stay the same.
+	\item Makes sure that the postcondition is satisfied by stating there
+		are $a_i$ and $a_j$ where $i\neq j$ and $a_i^N=a_j^N$ and both
+		are bigger then $50$
+\end{enumerate}
+
+\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:a4.py}. The Python
+script optimizes a little bit from the original formula by leaving out the
+$i=j$ comparison in subformula 17 and 18 by removing them from the set 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}.
+
+\lstinputlisting[language=bash,
+	caption={Iteratively find the shortest solution for problem 4},
+	label={listing:4.bash}]{src/a4.bash}
+
+\subsection{Solution}
+The bash script finds and shows the minimal solution in which the postcondition
+is satisfied for $N=11$. Finding this solution takes less then $75$ seconds and
+is shown in Table~\ref{tab:s4}.
+
+Every line in the table represents the iteration and the bold items represent
+the step chosen in transition between iterations.
+\begin{table}[H]
+	\centering
+	$\begin{array}{cc|ccccc}
+		\toprule
+		n & i & a_2 & a_3 & a_4 & a_5 & a_6\\
+		\midrule
+		0 & - & 2 & 3 & 4 & 5 & 6\\
+		1 & 4 & 2 & 3 & \mathbf{8} & 5 & 6\\
+		2 & 5 & 2 & 3 & 8 & \mathbf{14} & 6\\
+		3 & 2 & \mathbf{4} & 3 & 8 & 14 & 6\\
+		4 & 4 & 4 & 3 & \mathbf{17} & 14 & 6\\
+		5 & 5 & 4 & 3 & 17 & \mathbf{23} & 6\\
+		6 & 6 & 4 & 3 & 17 & 23 & \mathbf{30}\\
+		7 & 5 & 4 & 3 & 17 & \mathbf{47} & 30\\
+		8 & 4 & 4 & 3 & \mathbf{50} & 47 & 30\\
+		9 & 3 & 4 & \mathbf{54} & 50 & 47 & 30\\
+		10 & 6 & 4 & 54 & 50 & 47 & \mathbf{54}\\
+		\bottomrule
+	\end{array}$
+\caption{Solution table for problem 4}
+\label{tab:s4}
+\end{table}
diff --git a/ar/assignment1/Makefile b/ar/assignment1/Makefile
new file mode 100644
index 0000000..918eb44
--- /dev/null
+++ b/ar/assignment1/Makefile
@@ -0,0 +1,18 @@
+LATEX:=pdflatex
+
+DOCUMENT:=ar
+SOURCES:=$(filter-out preamble.tex,$(shell ls *.tex))
+
+.SECONDARY: $(addsuffix .fmt,$(DOCUMENT))
+
+all: $(DOCUMENT).pdf
+
+%.pdf: %.tex %.fmt $(SOURCES)
+	$(LATEX) $(basename $@)
+	$(LATEX) $(basename $@)
+
+%.fmt: preamble.tex
+	$(LATEX) -ini -jobname="$(basename $@)" "&$(LATEX) $<\dump"
+
+clean:
+	$(RM) -v $(addprefix $(DOCUMENT).,fmt aux log out toc pdf)
diff --git a/ar/assignment1/a.tex b/ar/assignment1/a.tex
new file mode 100644
index 0000000..e0ac8a3
--- /dev/null
+++ b/ar/assignment1/a.tex
@@ -0,0 +1,22 @@
+\section{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
+RAM: 8GB
+\end{lstlisting}
+
+\newpage
+\lstinputlisting[language=lisp,caption={a1.smt},
+	label={listing:a1.smt}]{src/a1.smt}
+
+\newpage
+\lstinputlisting[language=python,caption={a2.py},
+	label={listing:a2.py}]{src/a2.py}
+
+\newpage
+\lstinputlisting[language=python,caption={a3.py},
+	label={listing:a3.py}]{src/a3.py}
+
+\newpage
+\lstinputlisting[language=python,caption={a4.py},
+	label={listing:a4.py}]{src/a4.py}
diff --git a/ar/assignment1/ar.tex b/ar/assignment1/ar.tex
new file mode 100644
index 0000000..94e25f9
--- /dev/null
+++ b/ar/assignment1/ar.tex
@@ -0,0 +1,21 @@
+%&ar
+\begin{document}
+\maketitle
+\tableofcontents
+
+\newpage
+\input{1.tex}
+
+\newpage
+\input{2.tex}
+
+\newpage
+\input{3.tex}
+
+\newpage
+\input{4.tex}
+
+\newpage
+\input{a.tex}
+
+\end{document}
diff --git a/ar/assignment1/preamble.tex b/ar/assignment1/preamble.tex
new file mode 100644
index 0000000..5d2db97
--- /dev/null
+++ b/ar/assignment1/preamble.tex
@@ -0,0 +1,30 @@
+\documentclass{article}
+
+\usepackage{hyperref}	% For clickable links
+\usepackage{a4wide}	% For better page usage
+\usepackage{float}	% For better placement of tables/figures
+\usepackage{graphicx}	% For images
+\usepackage{amsmath}	% For align
+\usepackage{listings}	% For code snippets
+\usepackage{nicefrac}	% For diagonal fractions
+\usepackage{booktabs}	% For nice tables
+
+\everymath{\displaystyle\allowdisplaybreaks}
+
+\lstset{%
+  basicstyle=\scriptsize,
+  breakatwhitespace=true,
+  breaklines=true,
+  keepspaces=true,
+  numbers=left,
+  numberstyle=\tiny,
+  frame=L,
+  showspaces=false,
+  showstringspaces=false,
+  showtabs=false,
+  tabsize=2
+}
+
+\author{Mart Lubbers (s4109503)}
+\title{Automated reasoning Assignment 1} 
+\date{\today}
diff --git a/ar/assignment1/prnijm.pdf b/ar/assignment1/prnijm.pdf
new file mode 100644
index 0000000..a65fb82
Binary files /dev/null and b/ar/assignment1/prnijm.pdf differ
diff --git a/ar/assignment1/s2.png b/ar/assignment1/s2.png
new file mode 100644
index 0000000..2876b39
Binary files /dev/null and b/ar/assignment1/s2.png differ
diff --git a/ar/assignment1/s3.png b/ar/assignment1/s3.png
new file mode 100644
index 0000000..46e9e75
Binary files /dev/null and b/ar/assignment1/s3.png differ
diff --git a/ar/assignment1/src/a1.bash b/ar/assignment1/src/a1.bash
new file mode 100644
index 0000000..5ef0e5f
--- /dev/null
+++ b/ar/assignment1/src/a1.bash
@@ -0,0 +1,7 @@
+i=1
+while [ $(sed "s/<REP>/$i/g" a1.smt | 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))"
+sed "s/<REP>/$((i-1))/g" a1.smt | yices-smt -m
diff --git a/ar/assignment1/src/a1.smt b/ar/assignment1/src/a1.smt
new file mode 100644
index 0000000..cf5342e
--- /dev/null
+++ b/ar/assignment1/src/a1.smt
@@ -0,0 +1,60 @@
+(benchmark a1.smt
+:logic QF_UFLIA
+:extrafuns (
+	(t1p Int) (t1n Int) (t1s Int) (t1c Int) (t1d Int)
+	(t2p Int) (t2n Int) (t2s Int) (t2c Int) (t2d Int)
+	(t3p Int) (t3n Int) (t3s Int) (t3c Int) (t3d Int)
+	(t4p Int) (t4n Int) (t4s Int) (t4c Int) (t4d Int)
+	(t5p Int) (t5n Int) (t5s Int) (t5c Int) (t5d Int)
+	(t6p Int) (t6n Int) (t6s Int) (t6c Int) (t6d Int)
+)
+:formula
+(and
+	(>= t1p 0) (>= t1n 0) (>= t1s 0) (>= t1c 0) (>= t1d 0)
+	(>= t2p 0) (>= t2n 0) (>= t2s 0) (>= t2c 0) (>= t2d 0)
+	(>= t3p 0) (>= t3n 0) (>= t3s 0) (>= t3c 0) (>= t3d 0)
+	(>= t4p 0) (>= t4n 0) (>= t4s 0) (>= t4c 0) (>= t4d 0)
+	(>= t5p 0) (>= t5n 0) (>= t5s 0) (>= t5c 0) (>= t5d 0)
+	(>= t6p 0) (>= t6n 0) (>= t6s 0) (>= t6c 0) (>= t6d 0)
+
+	(<= (+ t1p t1n t1s t1c t1d) 8)
+	(<= (+ t2p t2n t2s t2c t2d) 8)
+	(<= (+ t3p t3n t3s t3c t3d) 8)
+	(<= (+ t4p t4n t4s t4c t4d) 8)
+	(<= (+ t5p t5n t5s t5c t5d) 8)
+	(<= (+ t6p t6n t6s t6c t6d) 8)
+
+	(<= (+ (* t1n 700) (* t1p 800) (* t1s 1000) (* t1c 1500) (* t1d 100)) 7800)
+	(<= (+ (* t2n 700) (* t2p 800) (* t2s 1000) (* t2c 1500) (* t2d 100)) 7800)
+	(<= (+ (* t3n 700) (* t3p 800) (* t3s 1000) (* t3c 1500) (* t3d 100)) 7800)
+	(<= (+ (* t4n 700) (* t4p 800) (* t4s 1000) (* t4c 1500) (* t4d 100)) 7800)
+	(<= (+ (* t5n 700) (* t5p 800) (* t5s 1000) (* t5c 1500) (* t5d 100)) 7800)
+	(<= (+ (* t6n 700) (* t6p 800) (* t6s 1000) (* t6c 1600) (* t6d 100)) 7800)
+
+	(or (= 0 t1p) (= 0 t1c))
+	(or (= 0 t2p) (= 0 t2c))
+	(or (= 0 t3p) (= 0 t3c))
+	(or (= 0 t4p) (= 0 t4c))
+	(or (= 0 t5p) (= 0 t5c))
+	(or (= 0 t6p) (= 0 t6c))
+
+	(<= t1d 1)
+	(<= t2d 1)
+	(<= t3d 1)
+	(<= t4d 1)
+	(<= t5d 1)
+	(<= t6d 1)
+
+	(= t3s 0)
+	(= t4s 0)
+	(= t5s 0)
+	(= t6s 0)
+
+	(= (+ t1n t2n t3n t4n t5n t6n) 4)
+	(= (+ t1s t2s t3s t4s t5s t6s) 8)
+	(= (+ t1c t2c t3c t4c t5c t6c) 10)
+	(= (+ t1d t2d t3d t4d t5d t6d) 5)
+
+	(>= (+ t1p t2p t3p t4p t5p t6p) <REP>)
+)
+)
diff --git a/ar/assignment1/src/a2.bash b/ar/assignment1/src/a2.bash
new file mode 100644
index 0000000..5462573
--- /dev/null
+++ b/ar/assignment1/src/a2.bash
@@ -0,0 +1 @@
+python3 a2.py | yices-smt -m
diff --git a/ar/assignment1/src/a2.py b/ar/assignment1/src/a2.py
new file mode 100644
index 0000000..85473a3
--- /dev/null
+++ b/ar/assignment1/src/a2.py
@@ -0,0 +1,66 @@
+#!/usr/bin/env python3
+pc = [(4, 2), (4, 2), (4, 2)]
+rc = [(9, 7), (12, 6), (10, 7), (18, 5), (20, 4), (10, 6), (8, 6), (10, 8)]
+mx = 29
+my = 22
+pd = 17
+
+# Print preamble
+print("(benchmark a4.smt")
+print(":logic QF_UFLIA")
+
+# Print variables
+print(":extrafuns (")
+for i, (w, h) in enumerate(pc+rc, 1):
+    print("(c{}x Int)".format(i), end=' ')
+    print("(c{}y Int)".format(i), end=' ')
+    print("(c{}w Int)".format(i), end=' ')
+    print("(c{}h Int)".format(i))
+print(")")
+
+print(":formula")
+print("(and")
+
+# Print the PC and RC subformulas
+for i, (w, h) in enumerate(pc+rc, 1):
+    # Print the width and height
+    print(('(or '
+           '(and (= c{0}w {1}) (= c{0}h {2})) '
+           '(and (= c{0}w {2}) (= c{0}h {1})))').format(i, w-1, h-1))
+    # Print the bounds of the coordinates
+    print(('(> c{0}x 0) (> c{0}y 0)'
+           '(<= (+ c{0}x c{0}w) {1}) (<= (+ c{0}y c{0}h) {2})'
+           ).format(i, mx, my))
+
+    # Print the non overlap with others
+    for j in range(1, 1+len(pc+rc)):
+        if i != j:
+            print((
+                 '(or '
+                 '(> c{0}x (+ c{1}x c{1}w)) (< (+ c{0}x c{0}w) c{1}x) '
+                 '(> c{0}y (+ c{1}y c{1}h)) (< (+ c{0}y c{0}h) c{1}y)'
+                 ')').format(i, j))
+
+# Print the PC distance to eachother
+for i, _ in enumerate(pc, 1):
+    for j, _ in enumerate(pc, 1):
+        if i != j:
+            print(('(or '
+                   '(> (- (+ c{0}x (/ c{0}w 2)) (+ c{1}x (/ c{1}w 2))) {2}) '
+                   '(> (- (+ c{1}x (/ c{1}w 2)) (+ c{0}x (/ c{0}w 2))) {2}) '
+                   '(> (- (+ c{0}y (/ c{0}h 2)) (+ c{1}y (/ c{1}h 2))) {2}) '
+                   '(> (- (+ c{1}y (/ c{1}h 2)) (+ c{0}y (/ c{0}h 2))) {2})'
+                   ')').format(i, j, pd))
+
+            # Print the constraint that they have to be connected to a ps
+for i, _ in enumerate(rc, 1+len(pc)):
+    print('(or')
+    for j, _ in enumerate(pc, 1):
+        print(('(not (or '
+               '(> c{0}x (+ c{1}x 1 c{1}w)) (< (+ c{0}x c{0}w) (- c{1}x 1)) '
+               '(> c{0}y (+ c{1}y 1 c{1}h)) (< (+ c{0}y c{0}h) (- c{1}y 1))'
+               '))').format(i, j))
+    print(')')
+
+# Close the and,benchmark parenthesis
+print("))")
diff --git a/ar/assignment1/src/a3.bash b/ar/assignment1/src/a3.bash
new file mode 100644
index 0000000..0a21dee
--- /dev/null
+++ b/ar/assignment1/src/a3.bash
@@ -0,0 +1,7 @@
+i=1
+while [ $(python3 a3.py $i | yices-smt) = "unsat" ]; do
+	echo "T=$i is still unsat"
+	i=$((i+1))
+done
+echo "T=$i is sat thus the minimum T=$i"
+python3 a3.py $i | yices-smt -m
diff --git a/ar/assignment1/src/a3.py b/ar/assignment1/src/a3.py
new file mode 100644
index 0000000..7d79135
--- /dev/null
+++ b/ar/assignment1/src/a3.py
@@ -0,0 +1,47 @@
+#!/usr/bin/env python3
+import sys
+
+if len(sys.argv) != 2:
+    print('usage: {} maxjobstart'.format(sys.argv[0]))
+    exit()
+
+maxjobstart = sys.argv[1]
+jobs = 12
+J = range(1, jobs+1)
+Jprime = {5, 7, 10}
+pi = {
+    3: {1, 2},
+    5: {3, 4},
+    7: {3, 4, 6},
+    9: {5, 8},
+    11: {10},
+    12: {9, 11}
+}
+
+# Print preamble
+print('(benchmark a4.smt')
+print(':logic QF_UFLIA')
+
+# Print variables
+print(':extrafuns (')
+for i in J:
+    print('(j{} Int)'.format(i), end=' ')
+print('\n)')
+
+print(':formula')
+print('(and')
+for i in J:
+    # Make sure the times are positive and within the bound
+    print('(> j{0} 0) (<= (+ j{0} {0}) {1})'.format(i, maxjobstart))
+    # Make sure the dependencies are done when a task is scheduled
+    for k in pi.get(i, {}):
+        print('(>= j{0} (+ j{1} {1}))'.format(i, k))
+# Make sure the shared resources are not used by two tasks at once
+for i in Jprime:
+    for k in Jprime:
+        if i != k:
+            print('(or (>= j{0} (+ j{1} {1}))'.format(i, k), end=' ')
+            print('(<= (+ j{0} {0}) j{1}))'.format(i, k))
+
+# Close the and,benchmark parenthesis
+print('))')
diff --git a/ar/assignment1/src/a4.bash b/ar/assignment1/src/a4.bash
new file mode 100644
index 0000000..23abab8
--- /dev/null
+++ b/ar/assignment1/src/a4.bash
@@ -0,0 +1,7 @@
+i=1
+while [ $(python3 a4.py $i | yices-smt) = "unsat" ]; do
+	echo "N=$i is still unsat"
+	i=$((i+1))
+done
+echo "N=$i is sat thus minimum N=$i"
+python3 a4.py $i | yices-smt -m
diff --git a/ar/assignment1/src/a4.py b/ar/assignment1/src/a4.py
new file mode 100644
index 0000000..f33f57c
--- /dev/null
+++ b/ar/assignment1/src/a4.py
@@ -0,0 +1,55 @@
+#!/usr/bin/env python3
+import sys
+if len(sys.argv) != 2:
+    print("usage: {} maxiterations".format(sys.argv[0]))
+    exit()
+
+iterations = int(sys.argv[1]) if len(sys.argv) > 1 else 11
+numa = 7
+
+# Print preamble
+print("(benchmark a4.smt")
+print(":logic QF_UFLIA")
+
+# Print variables
+print(":extrafuns (")
+print("(a{} Int)".format(1))
+print("(a{} Int)".format(numa))
+for i in range(iterations):
+    for v in range(2, numa):
+        print("(i{}a{} Int) ".format(i, v))
+print(")")
+
+# Print preconditions
+print(":formula")
+print("(and")
+print("(= a1 1)")
+print("(= a{0} {0})".format(numa, numa))
+for i in range(2, numa):
+    print("(= i0a{0} {0})".format(i))
+
+# Print iterations
+for i in range(1, iterations):
+    print("(or")
+    for v in range(2, numa):
+        print("(and")
+        for ov in [k for k in range(2, numa) if k != v]:
+            print("(= i{0}a{1} i{2}a{1})".format(i, ov, i-1))
+        im1 = 'a1' if v == 2 else 'i{}a{}'.format(i, v-1)
+        ip1 = 'a{}'.format(numa) if v == numa-1 else 'i{}a{}'.format(i-1, v+1)
+        print("(= i{}a{} (+ {} {}))".format(i, v, im1, ip1))
+        print(")")
+    print(")")
+
+#  Post conditions
+print("(or")
+for v in range(2, numa):
+    print("(and (>= i{}a{} 50)".format(iterations-1, v))
+    print("(or")
+    for ov in [k for k in range(2, numa) if k != v]:
+        print("(= i{0}a{1} i{0}a{2})".format(iterations-1, v, ov))
+    print("))")
+print(")")
+
+#  Close the and,benchmark parenthesis
+print("))")