The Sokoban Editor is a planning as satisfiability solver for Sokoban. It based on Snowman-Editor, but much more simpler.
The editor can solve a given level optimally using the Yices SMT.
Download the latest version from the release page or build the project.
The editor requires at least Java SE 11.
First execution to generate the config file:
java -jar sokoban_editor.jar
Once the config file has been generated, set the Yices 2 solver path.
To solve a given level:
java -jar sokoban_editor.jar smt_reachability ./levels/toy/toy5.lvl
Where:
- smt_basic - minimizes character + box movements.
- smt_reachability - minimizes box movements guaranteeing valid character movements.
- smt_reachability_folding - minimizes change of directions of box movements (box movement of n positions in a straight line has a cost of 1).
Download the source code:
git clone https://github.com/GerardMT/Sokoban-Editor
cd Sokoban-Editor
Download the Planner submodule:
git submodule update --init --recursive
The project uses the SBT build tool. To compile the project run:
sbt compile
sbt assembly
The package output can be found at ./out/sokoban_editor.jar.
I personally use IntelliJ IDEA which eases the Scala/Java environment setup.
Execution of:
java -jar sokoban_editor. jar smt_reachability ./levels/microban/levels/microban1.lvl
Output:
timesteps=1 time=525
timesteps=2 time=276
timesteps=3 time=155
timesteps=4 time=152
timesteps=5 time=107
timesteps=6 time=126
timesteps=7 time=197
timesteps=8 time=242
STATE 0
####xx
# .#xx
# ###
#*@ #
# $ #
# ###
####xx
...
STATE 7
####xx
# .#xx
# $###
#*@ #
# #
# ###
####xx
STATE 8
####xx
# *#xx
# @###
#* #
# #
# ###
####xx
plan=dlUrrrdLullddrUluRuulDrddrruLdlUU
lenght=33
box_actions=8
time=2.07