From c42bd24200f0783113e1e29f5af519fdb0d9ba47 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Fri, 15 Apr 2016 20:40:09 +0200 Subject: [PATCH] Started with report --- report2/.gitignore | 4 ++ report2/Makefile | 17 ++++++ report2/implementation.tex | 105 +++++++++++++++++++++++++++++++++++++ report2/pre.tex | 16 ++++++ report2/report.tex | 7 +++ report2/results.tex | 0 6 files changed, 149 insertions(+) create mode 100644 report2/.gitignore create mode 100644 report2/Makefile create mode 100644 report2/implementation.tex create mode 100644 report2/pre.tex create mode 100644 report2/report.tex create mode 100644 report2/results.tex diff --git a/report2/.gitignore b/report2/.gitignore new file mode 100644 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 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 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 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 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 index 0000000..e69de29 -- 2.20.1