Started with report

diff --git a/report2/.gitignore b/report2/.gitignore
new file mode 100644 (file)
index 0000000..d8b763f
--- /dev/null
+++ b/report2/.gitignore
@@ -0,0 +1,4 @@
+*.pdf
+*.log
+*.aux
+*.fmt

diff --git a/report2/Makefile b/report2/Makefile
new file mode 100644 (file)
index 0000000..66efe76
--- /dev/null
+++ b/report2/Makefile
@@ -0,0 +1,17 @@
+LATEX:=pdflatex
+DOCUMENT:=report
+
+.PHONY: all clean
+.SECONDARY: $(DOCUMENT).fmt
+
+all: $(DOCUMENT).pdf
+
+%.pdf: %.tex %.fmt implementation.tex results.tex
+       $(LATEX) $<
+       $(LATEX) $<
+
+%.fmt: pre.tex
+       $(LATEX) -ini -shell-escape -jobname="$(basename $@)" "&$(LATEX) $<\dump"
+
+clean:
+       $(RM) -rv $(addprefix $(DOCUMENT).,fmt log aux pdf)

diff --git a/report2/implementation.tex b/report2/implementation.tex
new file mode 100644 (file)
index 0000000..04893f7
--- /dev/null
+++ b/report2/implementation.tex
@@ -0,0 +1,105 @@
+\section{Implementation}
+\subsection{Screen encoding}
+When parsed the sokoban screen is stripped of all walls and unreachable empty
+spaces are removed.
+
+Let $T=\{free,box,target,agent,targetagent,targetbox\}$ be the set of
+possible states of a tile. Tiles are numbered and thus a sokoban screen is the
+set $F$ containing a $x_i\in T$ for every tile. To encode the state we
+introduce an encoding function that encodes a state in three boolean variables:
+$$encode(t)=\begin{cases}
+       000 & \text{if }t=wall\\
+       001 & \text{if }t=free\\
+       010 & \text{if }t=box\\
+       011 & \text{if }t=target\\
+       100 & \text{if }t=targetbox\\
+       101 & \text{if }t=agent\\
+       110 & \text{if }t=agentbox
+\end{cases}$$
+
+This means that the encoding of a screen takes $3*|F|$ variables.
+
+\subsection{Transition encoding}
+We introduce a variable denoting the intended direction of movement $m \in
+\{\text{up}, \text{down}, \text{left}, \text{right}\}$. 
+%
+%Let\\
+%$\delta_{x}(x,m) =
+%  \begin{cases}
+%    (x+1) & \quad \text{if } m = left\\
+%    (x-1) & \quad \text{if } m = right\\
+%    x & \quad \text{otherwise}
+%  \end{cases}$\quad
+%$\delta'_{x}(x,m) =
+%  \begin{cases}
+%    (x-1) & \quad \text{if } m = left\\
+%    (x+1) & \quad \text{if } m = right\\
+%    x & \quad \text{otherwise}
+%  \end{cases}$\\
+%$\delta_{y}(y,m) =
+%  \begin{cases}
+%    (y+1) & \quad \text{if } m = up\\
+%    (y-1) & \quad \text{if } m = down\\
+%    y & \quad \text{otherwise}
+%  \end{cases}$\quad
+%$\delta'_{y}(y,m) =
+%  \begin{cases}
+%    (y-1) & \quad \text{if } m = up\\
+%    (y+1) & \quad \text{if } m = down\\
+%    y & \quad \text{otherwise}
+%  \end{cases}$\\
+%  $\gamma_{x}(x,m) =
+%    \begin{cases}
+%      (x+2) & \quad \text{if } m = left\\
+%      (x-2) & \quad \text{if } m = right\\
+%      x & \quad \text{otherwise}
+%    \end{cases}$\quad
+%  $\gamma_{y}(y,m) =
+%    \begin{cases}
+%      (y+2) & \quad \text{if } m = up\\
+%      (y-2) & \quad \text{if } m = down\\
+%      y & \quad \text{otherwise}
+%    \end{cases}$
+%
+%%    "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = Agent | x"
+%%                            <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = AgentOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Free | x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Target) & move = Left: AgentOnTarget;",
+%%                    "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Agent | x"
+%%                            <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = AgentOnTarget) & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Free | x" <+ (checkX p (x-1)) <+ "_"
+%%                            <+ (checkY p (x-1) y) <+ " = Target) & move = Up: AgentOnTarget;",
+%%                    "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = Agent | x"
+%%                            <+ (checkX p x) <+ "_" <+ (checkY p x (y-1)) <+ " = AgentOnTarget) & (x" <+ (checkX p x) <+ "_" <+ (checkY p x  (y+1)) <+ " = Free | x" <+ x <+ "_" <+ (checkY p x  (y+1)) <+ " = Target) & move = Right : AgentOnTarget;",
+%%                    "    x" <+ x <+ "_" <+ y <+ " = BoxOnTarget & (x" <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = Agent | x"
+%%                            <+ (checkX p (x-1)) <+ "_" <+ (checkY p (x-1) y) <+ " = AgentOnTarget) & (x" <+ (checkX p (x+1)) <+ "_" <+ (checkY p (x+1) y) <+ " = Free | x" <+ (checkX p (x+1)) <+ "_"
+%%                            <+ (checkY p (x+1) y) <+ " = Target) & move = Down : AgentOnTarget;",
+%
+%
+%
+%We define the tile update function $next(x_{i,j}), x_{i,j} \in F, \forall i,j \text{ s.t.} x_{i,j} \neq \perp$ as\\
+%$
+%next(x_{i,j}) =
+%  \begin{cases}
+%    \# & \quad \text{if } x_{i,j} = \#\\
+%    @ & \quad \text{if } x_{i,j} = \_ \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = @ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = +) \wedge x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp\\
+%    @ & \quad \text{if } x_{i,j} = \$ \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = @ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = +)\\
+%    & \quad \wedge (x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = \_ \vee x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = .)\\
+%    & \quad \wedge x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp \wedge x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} \neq \perp\\
+%    \$ & \quad \text{if } x_{i,j} = \_ \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = \$ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = *)\\ & \quad \wedge (x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = @ \vee x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = +) \wedge x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp \wedge x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} \neq \perp\\
+%    \_ & \quad \text{if } x_{i,j} = @ \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = \_ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = .)\\
+%    & \quad \vee ((x_{\delta_{x}(i,m),\delta_{y}(j,m)} = \$ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = *) \wedge \\
+%    & \quad (x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = \_ \vee x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = .)) \\
+%    & \quad x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp \wedge x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} \neq \perp\\
+%    + & \quad x_{i,j} = . \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = @ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = +) \wedge x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp\\
+%    + & \quad x_{i,j} = * \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = @ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = +)\\
+%    & \quad \wedge (x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = \_ \vee x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} = .)\\
+%    & \quad \wedge x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp \wedge x_{\delta'_{x}(i,m),\delta'_{y}(j,m)} \neq \perp\\
+%    * & \quad \text{if } x_{i,j} = . \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = \$ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = *)\\
+%    & \quad \wedge (x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = @ \vee x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} = +)\\
+%    & \quad \wedge x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp \wedge x_{\gamma_{x}(i,m),\gamma_{y}(j,m)} \neq \perp\\
+%    . & \quad x_{i,j} = + \wedge (x_{\delta_{x}(i,m),\delta_{y}(j,m)} = \_ \vee x_{\delta_{x}(i,m),\delta_{y}(j,m)} = .) \wedge x_{\delta_{x}(i,m),\delta_{y}(j,m)} \neq \perp\\
+%    x_{i,j} & \quad \text{otherwise}\\
+%  \end{cases}
+%$
+%\subsection{Goal}
+%Let $G = \{z_{i,j} | z_{i,j} \in F, \forall i,j \text{ s.t.} z_{i,j} \in \{.,*\}\}$ be a subset of $F$.
+%In order to check a sokoban field for a possible solution, we introduce the following invariant:\\
+%$$\neg \bigwedge_{x \in G} (x = *)$$

diff --git a/report2/pre.tex b/report2/pre.tex
new file mode 100644 (file)
index 0000000..0320a7f
--- /dev/null
+++ b/report2/pre.tex
@@ -0,0 +1,16 @@
+\documentclass{article}
+
+\usepackage{a4wide}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{listings}
+
+\lstset{%
+       breaklines,
+       basicstyle=\scriptsize
+}
+
+\title{Solving Sokoban using BDDs powered by
+       \textsc{Sylvan}~\footnote{https://github.com/utwente-fmt/sylvan}}
+\author{Alexander Fedotov (s4460952)\and Mart Lubbers (s4109503)}
+\date{\today}

diff --git a/report2/report.tex b/report2/report.tex
new file mode 100644 (file)
index 0000000..7f2ce0f
--- /dev/null
+++ b/report2/report.tex
@@ -0,0 +1,7 @@
+%&report
+\begin{document}
+\maketitle
+\input{implementation.tex}
+
+\input{results.tex}
+\end{document}

diff --git a/report2/results.tex b/report2/results.tex
new file mode 100644 (file)
index 0000000..e69de29