Sokoban Solver in Copris

Table of Contents

Overview

This page presents a Sokoban solver written in Copris, a Constraint Programming DSL (Domain-Specific Language) embedded in Scala. Sokoban is a puzzle game developed by Hiroyuki Imabayashi of Thinking Rabbit software house in Japan.

This Sokoban solver can find a solution or a solution with a minimum number of pushes for the given puzzle .

What's New

  • 2013-10-14 Mon Release of version 1.1
  • 2013-09-01 Sun First release

Download

Version 1.1
Version 1.0

Requirements

  • Scala version 2.10 to be installed
    • Scala version 2.9 is not binary compatible with version 2.10. You need to compile Copris from the source.
  • Copris (included in the package)
  • Sugar (included in the package)
  • Sat4j Core (included in the package)

How to use

scala -cp copris-sokoban-v1-1.jar sokoban.Solver input_file_name
  • The format of the input file is explained below.

To find a solution with a minimum number of pushes, please use "-o opt" option.

scala -cp copris-sokoban-v1-1.jar sokoban.Solver -o opt input_file_name

If you have a SAT solver (such as clasp, MiniSat, Glucose, GlueMiniSat) installed on your computer, you can use it to get better performance.

scala -cp copris-sokoban-v1-1.jar sokoban.Solver -o opt -s2 minisat input_file_name

Input file format

The following is an example of input file.

7
6
######
# .###
#  ###
#*@  #
#  $ #
#  ###
######
  • The first line gives the number of rows.
  • The second line gives the number of columns.
  • See SokobanWiki:Level format for more details.

Example Usage

$ scala -cp copris-sokoban-v1-0.jar sokoban.Solver -v -o opt -s2 minisat data/m1-00001.txt
File = data/m1-00001.txt
Solver = minisat
Options = opt
Rows = 7
Cols = 6
Steps = 8
Step = 0
######
# .###
#  ###
#*@  #
#  $ #
#  ###
######
Step = 1
######
# .###
#$ ###
#+   #
#  $ #
#  ###
######
Step = 2
######
# .###
#$ ###
#.   #
# $@ #
#  ###
######
Step = 3
######
# .###
#$ ###
#.$  #
# @  #
#  ###
######
Step = 4
######
# .###
#$ ###
#.@$ #
#    #
#  ###
######
Step = 5
######
# .###
#@ ###
#* $ #
#    #
#  ###
######
Step = 6
######
# .###
#  ###
#*$@ #
#    #
#  ###
######
Step = 7
######
# .###
# $###
#*@  #
#    #
#  ###
######
Step = 8
######
# *###
# @###
#*   #
#    #
#  ###
######

Performance Evaluation

Solver performance is measured on version 1.0.

  • Copris solver was run on Intel Xeon 3.33GHz machine with:
    • Ubuntu Linux 12.04 (64 bit)
    • Java version "1.6.0_27", OpenJDK Runtime Environment (with "-Xmx4G" option)
    • Scala version 2.9.1
    • Copris version 2.0.0
    • Sugar version 2.0.0
  • Glucose version 2.1 (with preprocessing) is used as a SAT solver.

Finding a solution

  • We used 155 instances of Microban by David W. Skinner.
  • 17 instances were not solved within 3600 seconds.
  • The average time of 138 solved instances was about 161.6 seconds. The longest time was about 3435.9 seconds.
  • See runall-godel-v10-first-glucose21_simp.log for more details.

Finding a solution with a minimum number of pushes

  • We used 155 instances of Microban by David W. Skinner.
  • 25 instances were not solved within 3600 seconds.
  • The average time of 130 solved instances was about 282.1 seconds. The longest time was about 2761.7 seconds.
  • See runall-godel-v10-opt-glucose21_simp.log for more details.

Source Code

The following shows the source code of the solver (Sokoban-v1-1.scala).

  1:  /*
  2:   * Sokoban Solver in Copris
  3:   * by Naoyuki Tamura
  4:   * http://bach.istc.kobe-u.ac.jp/copris/puzzles/sokoban/
  5:   */
  6:  package sokoban
  7:  import jp.kobe_u.copris._
  8:  import jp.kobe_u.copris.dsl._
  9:  import scala.io.Source
 10:  
 11:  case class Puzzle(m: Int, n: Int, board: Seq[Seq[String]]) {
 12:    require(board.size == m && m >= 2)
 13:    require(board.forall(_.size == n) && n >= 2)
 14:    def isWall(i: Int, j: Int) = board(i)(j) == "#"
 15:    def isGoal(i: Int, j: Int) = board(i)(j).matches("""[\.\*\+]""")
 16:    def isPlayer(i: Int, j: Int) = board(i)(j).matches("""[\@\+]""")
 17:    def isBox(i: Int, j: Int) = board(i)(j).matches("""[o\*\$]""")
 18:    def isInside(i: Int, j: Int) = 0 <= i && i < m && 0 <= j && j < n && ! isWall(i, j)
 19:    val nodes = for (i <- 0 until m; j <- 0 until n; if ! isWall(i, j)) yield (i,j)
 20:    val dijs = Seq((-1,0), (1,0), (0,-1), (0,1))
 21:    def next(i: Int, j: Int) =
 22:      for ((di,dj) <- dijs; if isInside(i+di, j+dj)) yield (i+di,j+dj)
 23:    val badBlocks: Set[Set[(Int,Int)]] = {
 24:      val blocks = for {
 25:        (i,j) <- nodes.toSet
 26:        block = for ((i1,j1) <- Set((i,j), (i,j+1), (i+1,j), (i+1,j+1)); if isInside(i1, j1))
 27:                yield (i1,j1)
 28:        if block.exists(ij => ! isGoal(ij._1, ij._2))
 29:      } yield block
 30:      val blocks1 = blocks.filterNot(b1 => blocks.exists(b2 => b1.size > b2.size && b2.subsetOf(b1)))
 31:      blocks1
 32:    }
 33:    val deadBlocks: Set[Set[(Int,Int)]] = {
 34:      val hBlocks = for {
 35:        (i,j) <- nodes.toSet
 36:        if isWall(i, j-1)
 37:        len <- 2 until n-1
 38:        if j+len < n && isWall(i, j+len) && (0 until len).forall(k => isInside(i, j+k))
 39:        if (0 until len).forall(k => isWall(i-1, j+k) || isWall(i+1, j+k))
 40:      } yield (0 until len).map(k => (i, j+k)).toSet
 41:      val vBlocks = for {
 42:        (i,j) <- nodes.toSet
 43:        if isWall(i-1, j)
 44:        len <- 2 until m-1
 45:        if i+len < m && isWall(i+len, j) && (0 until len).forall(k => isInside(i+k, j))
 46:        if (0 until len).forall(k => isWall(i+k, j-1) || isWall(i+k, j+1))
 47:      } yield (0 until len).map(k => (i+k, j)).toSet
 48:      hBlocks ++ vBlocks
 49:    }
 50:  }
 51:  
 52:  object Solver {
 53:    val name = "sokoban.Solver"
 54:    var help = false
 55:    var quiet = 0
 56:    var verbose = 0
 57:    var options: Set[String] = Set.empty
 58:    var puzzle: Puzzle = null
 59:  
 60:    def parse(source: Source) = {
 61:      val lines = source.getLines.map(_.trim)
 62:      val m = lines.next.toInt
 63:      val n = lines.next.toInt
 64:      val board = for (i <- 0 until m; s = lines.next)
 65:                  yield s.map(_.toString)
 66:      source.close
 67:      new Puzzle(m, n, board)
 68:    }
 69:  
 70:    def define(minSteps: Int, maxSteps: Int) {
 71:      def declare(step: Int) {
 72:        // Player
 73:        int('pi(step), 0, puzzle.m-1); int('pj(step), 0, puzzle.n-1)
 74:        for (i <- 0 until puzzle.m; j <- 0 until puzzle.n) {
 75:          int('p(step,i,j), 0, 1)
 76:          add(('p(step,i,j) === 1) <==> ('pi(step) === i && 'pj(step) === j))
 77:          if (puzzle.isWall(i, j))
 78:            add('p(step,i,j) === 0)
 79:        }
 80:        // Boxes
 81:        for ((i,j) <- puzzle.nodes) {
 82:          int('b(step,i,j), 0, 1)
 83:          // add(('b(step,i,j) === 0) || ('p(step,i,j) === 0))
 84:        }
 85:        // Goal
 86:        int('g(step), 0, 1)
 87:        val gs = for ((i,j) <- puzzle.nodes; if puzzle.isGoal(i, j))
 88:          yield 'b(step,i,j) === 1
 89:        add(('g(step) === 1) <==> And(gs))
 90:        add(('steps <= step) ==> ('g(step) === 1))
 91:        // Hints
 92:        for (block <- puzzle.badBlocks)
 93:          add(! And(block.map(ij => 'b(step,ij._1,ij._2) === 1)))
 94:        for (block <- puzzle.deadBlocks) {
 95:          val count = block.count(ij => puzzle.isGoal(ij._1, ij._2))
 96:          val bs = for ((i,j) <- block) yield 'b(step,i,j)
 97:          add(Add(bs) <= count)
 98:        }
 99:      }
100:      def initial(step: Int) {
101:        for ((i,j) <- puzzle.nodes) {
102:          add('p(step,i,j) === (if (puzzle.isPlayer(i, j)) 1 else 0))
103:          add('b(step,i,j) === (if (puzzle.isBox(i, j)) 1 else 0))
104:        }
105:      }
106:      def reachability(step: Int) {
107:        for ((i,j) <- puzzle.nodes) {
108:          int('r(step,i,j), 0, 1)
109:          int('x(step,i,j), 0, puzzle.nodes.size)
110:          for ((i1,j1) <- puzzle.next(i, j))
111:            int('e(step,i1,j1,i,j), 0, 1)
112:          int('in(step,i,j), 0, 1)
113:        }
114:        for ((i,j) <- puzzle.nodes) {
115:          val in = for ((i1,j1) <- puzzle.next(i, j)) yield 'e(step,i1,j1,i,j)
116:          add('in(step,i,j) === Add(in))
117:          for ((i1,j1) <- puzzle.next(i, j))
118:            add(('e(step,i1,j1,i,j) === 1) ==> ('x(step,i1,j1) > 'x(step,i,j)))
119:          add(('p(step,i,j) === 1) ==> ('in(step,i,j) === 0))
120:          add(('p(step,i,j) === 0) ==> (('in(step,i,j) === 1) || ('x(step,i,j) === 0)))
121:          add(('b(step,i,j) === 1) ==> ('in(step,i,j) === 0))
122:          add(('r(step,i,j) === 1) <==> (('p(step,i,j) === 1) || ('in(step,i,j) > 0)))
123:        }
124:      }
125:      def transition(step0: Int, step1: Int) {
126:        // Player and Move
127:        int('di(step0), -1, 1)
128:        int('dj(step0), -1, 1)
129:        add(('g(step0) === 1) <==> (('di(step0) === 0) && ('dj(step0) === 0)))
130:        add((('di(step0) === 0) && ('dj(step0) === 0)) ==> (('pi(step0) === 'pi(step1)) && ('pj(step0) === 'pj(step1))))
131:        reachability(step0)
132:        for ((i,j) <- puzzle.nodes) {
133:          val push = for ((di,dj) <- puzzle.dijs; if puzzle.isInside(i-di, j-dj) && puzzle.isInside(i+di, j+dj))
134:                     yield ('di(step0) === di) && ('dj(step0) === dj) && ('r(step0,i-di,j-dj) === 1) && ('b(step0,i+di,j+dj) === 0)
135:          add(('p(step1,i,j) === 1) ==> (
136:                (('p(step0,i,j) === 1) && ('g(step0) === 1)) ||
137:                (('b(step0,i,j) === 1) && Or(push))))
138:        }
139:        // Blocks
140:        for ((i,j) <- puzzle.nodes) {
141:          val stay = ('b(step0,i,j) === 1) && ('p(step1,i,j) === 0)
142:          val push = for ((di,dj) <- puzzle.dijs; if puzzle.isInside(i-di, j-dj))
143:            yield ('di(step0) === di) && ('dj(step0) === dj) && ('b(step0,i-di,j-dj) === 1) && ('p(step1,i-di,j-dj) === 1)
144:          add(('b(step1,i,j) === 1) <==> (stay || Or(push)))
145:        }
146:      }
147:      int('steps, minSteps, maxSteps)
148:      declare(0)
149:      initial(0)
150:      for (step <- 1 to maxSteps) {
151:        declare(step)
152:        transition(step-1, step)
153:      }
154:    }
155:  
156:    def showSolution(steps: Int) {
157:      println("Steps = " + steps)
158:      for (step <- 0 to steps) {
159:        println("Step = " + step)
160:        for (i <- 0 until puzzle.m) {
161:          val cs = for (j <- 0 until puzzle.n) yield {
162:            if (puzzle.isWall(i, j)) "#"
163:            else if (solution('p(step,i,j)) > 0 && puzzle.isGoal(i, j)) "+"
164:            else if (solution('p(step,i,j)) > 0) "@"
165:            else if (solution('b(step,i,j)) > 0 && puzzle.isGoal(i, j)) "*"
166:            else if (solution('b(step,i,j)) > 0) "$"
167:            else if (puzzle.isGoal(i, j)) "."
168:            else " "
169:          }
170:          println(cs.mkString)
171:        }
172:      }
173:      println
174:    }
175:  
176:    def solve {
177:      var found = false
178:      var minSteps = 0
179:      var maxSteps = 4
180:      if (verbose >= 1) {
181:        println("Rows = " + puzzle.m)
182:        println("Cols = " + puzzle.n)
183:      }
184:      while (! found) {
185:        if (verbose >= 2) {
186:          println("Steps = " + minSteps + ".." + maxSteps)
187:        }
188:        init
189:        define(minSteps, maxSteps)
190:        if (find)
191:          found = true
192:        else {
193:          minSteps = maxSteps + 1
194:          maxSteps *= 2
195:        }
196:      }
197:      if (options.contains("opt")) {
198:        init
199:        define(minSteps, maxSteps)
200:        minimize('steps)
201:        if (findOpt)
202:          found = true
203:      }
204:      if (found) {
205:        val steps = solution('steps)
206:        showSolution(steps)
207:      }
208:    }
209:  
210:    def main(args: Array[String]) = {
211:      var fileName = ""
212:      var solverName = ""
213:      def parseOptions(args: List[String]): List[String] = args match {
214:        case "-o" :: opt :: rest =>
215:          { options = opt.split(",").toSet; parseOptions(rest) }
216:        case "-s1" :: solver :: rest => {
217:          solverName = solver
218:          val satSolver = new sugar.SatSolver1(solver)
219:          use(new sugar.Solver(csp, satSolver))
220:          parseOptions(rest)
221:        }
222:        case "-s2" :: solver :: rest => {
223:          solverName = solver
224:          val satSolver = new sugar.SatSolver2(solver)
225:          use(new sugar.Solver(csp, satSolver))
226:          parseOptions(rest)
227:        }
228:        case "-smt" :: solver :: rest => {
229:          solverName = solver
230:          val smtSolver = new smt.SmtSolver(solver)
231:          use(new smt.Solver(csp, smtSolver))
232:          parseOptions(rest)
233:        }
234:        case "-q" :: rest =>
235:          { quiet += 1; parseOptions(rest) }
236:        case "-v" :: rest =>
237:          { verbose += 1; parseOptions(rest) }
238:        case "-h" :: rest =>
239:          { help = true; parseOptions(rest) }
240:        case _ =>
241:          args
242:      }
243:      parseOptions(args.toList) match {
244:        case Nil if ! help => {
245:          fileName = "-"
246:          puzzle = parse(Source.stdin)
247:        }
248:        case file :: Nil if ! help => {
249:          fileName = file
250:          puzzle = parse(Source.fromFile(file))
251:        }
252:        case _ => {
253:          println("Usage: scala " + name + " [options] [inputFile]")
254:          println("\t-o options  : Set options")
255:          println("\t-v          : Increase verbosity level")
256:          println("\t-q          : Increase quiet level")
257:          println("\t-s1 solver  : Use SAT solver with one argument (clasp, etc.)")
258:          println("\t-s2 solver  : Use SAT solver with two arguments (minisat, etc.)")
259:          println("\t-smt solver : Use SMT solver (z3, etc.)")
260:          println("\t-dump file  : Output Sugar CSP to the specified file")
261:          println("\t-h          : Show this help message")
262:          System.exit(1)
263:        }
264:      }
265:      if (verbose >= 1) {
266:        println("File = " + fileName)
267:        println("Solver = " + solverName)
268:        println("Options = " + options.mkString(","))
269:      }
270:      solve
271:      if (verbose >= 2)
272:        println("Stats = " + stats)
273:    }
274:  }

License

This software is distributed under the BSD 3-Clause License. See LICENSE.txt.

Links

?????

Date: 2013-12-01 10:41:51 JST

Author: Naoyuki Tamura

Org version 7.8.02 with Emacs version 23

Validate XHTML 1.0