Solving Sokoban using BDDs powered by Sylvan ^{∗}

Alexander Fedotov (s4460952)  Mart Lubbers (s4109503)

April 21, 2016

Contents

1 Implementation 1 1.1 Screen encoding . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Transition encoding . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.3 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2

1.3.1 Encoding . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.3.2 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

2 Results & How-to 4 2.1 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.2 How-to . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

1 Implementation

1.1 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} ∈ T for every tile. We introduce a function ord(x, y) that returns the tile number for a given x and y coordinate and a function iord(i) that does the reverse. To encode the state we introduce an encoding function that encodes a state in three boolean variables:

encode(t) = \begin{cases}001 & if t = free \\ 010 & if t = box \\ 011 & if t = target \\ 100 & if t = targetbox \\ 101 & if t = agent \\ 110 & if t = agentbox \end{cases}

This means that the encoding of a screen takes 3 ∗ |F | variables.

1.2 Transition encoding

We introduce a variable denoting the intended direction of movement m ∈ {up, down, left, right}. Per move we define a δ and γ variable which represent the change in coordinate value respectively for the next position and the position next to the next postition.

∗https://github.com/utwente-fmt/sylvan

δ_{(x,y)}(m) = \begin{cases}(x − 1, y) & if m = left \\ (x + 1, y) & if m = right \\ (x, y + 1) & if m = down \\ (x, y − 1) & if m = up \end{cases} γ(x, y)(m) = \begin{cases}(x − 2, y) & if m = left \\ (x + 2, y) & if m = right \\ (x, y + 2) & if m = down \\ (x, y − 2) & if m = up \end{cases}

We define the tile update function next(i_{1}, i_{2}, i_{3}) where i_{1} contains the agent and i_{2} and i_{3} are adjacent to it in some direction.

next(i_{1}, i_{2}, i_{3}) = \{ \begin{matrix}(free, agent, box) & if & i_{1} = agent ∧ i_{2} = box ∧ i_{3} = free \\ (target, agent, box) & if & i_{1} = targetagent ∧ i_{2} = box ∧ i_{3} = free \\ (free, targetagent, box) & if & i_{1} = agent ∧ i_{2} = targetbox ∧ i_{3} = free \\ (free, agent, targetbox) & if & i_{1} = agent ∧ i_{2} = box ∧ i_{3} = targetbox \\ (target, targetagent, box) & if & i_{1} = targetagent ∧ i_{2} = targetbox ∧ i_{3} = free \\ (target, agent, targetbox) & if & i_{1} = targetagent ∧ i_{2} = box ∧ i_{3} = target \\ (free, targetagent, targetbox) & if & i_{1} = agent ∧ i_{2} = targetbox ∧ i_{3} = target \\ (target, targetagent, targetbox) & if & i_{1} = targetagent ∧ i_{2} = targetbox ∧ i_{3} = target \\ (free, agent, i_{3}) & if & i_{1} = agent ∧ i_{2} = free \\ (free, targetagent, i_{3}) & if & i_{1} = agent ∧ i_{2} = target \\ (target, agent, i_{3}) & if & i_{1} = targetagent ∧ i_{2} = free \\ (target, targetagent, i_{3}) & if & i_{1} = targetagent ∧ i_{2} = target \\ (agent, i_{2}, i_{3}) & if & i_{1} = agent \\ (targetagent, i_{2}, i_{3}) & if & i_{1} = targetagent \end{matrix}

1.3 Example

For example, take the toy screen shown in Listing 1. When the screen is parsed the unreachable space is first removed by detecting reachable space with the flood fill algorithm. This results in the minimized screen listed in Listing 2.

Listing 1: Example screen

###

#@$.#

###

Listing 2: Example screen

@$ .

1.3.1 Encoding

To encode the screen the tiles are numbered from left to right from top to bottom. Thus resulting in i_{1} = agent, i_{2} = box, i_{3} = target. When we translate these numbers to sylvan-sane variables we get the following bdd shown in Figure 1. Variables 0, 2, 4 represent i_{1}, 6, 8, 10 represent i_{2} and lastly 12, 14, 16 represents i_{3}.

Encoding the goal state happens in a similar way. The algorithm basically states that all target positions should be boxtarget. This is results in the BDD shown in Figure 2.

Finally encoding the transitions already results in a long list of complicated BDDs that each encode a possible move in all possible directions. In this example there is only one move possible in the first state, thus all moves except for the one move result in a relative product that is empty. For example the sub-BDD that encodes the first position only looks is visualized in Figure 3. The only satisfying assignment is that 0, 2, 4 hold the values 1, 0, 1 thus encoding man and the variables 1, 3, 5 holding the values 0, 0, 1 thus encoding free.

Figure 1: Initial state encoding of the example Figure 2: Goal state encoding of the example

Figure 3: Sub-BDD of a move 1.3.2 Results

2 Results & How-to

2.1 Results

This approach is not very efficient yet. While it is a bit faster than the previous NuSMV approach it is not capable of handling bigger screens.

Screen no. NuSMV This program
2000  n  n

2.2 How-to

The program can be built by running make. make expects the sylvan headers to be located in ./sylvan/src and the library archive in ./sylvan/src/libsylvan.a. If this is not the case one can adapt the makefile or set the appropriate CFLAGS and LDFLAGS.

When the main program is executed with the -h flag the help is shown. Note that the program is very silent when the -v flag is not set.

Usage :
. / main [ opts ] [ FILE ]
Options :
−l LURD LURD v e r i f i c a t i o n s t r a t e g y
−v  e n a b l e v e r b o s e output
−h  show t h i s help
P o s i t i o n a l arguments :
FILE  z e r o or one sokoban s c r e e n s
when no f i l e i s s p e c i f i e d s t d i n w i l l be used