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

  • 2020-12-15 Tue Release of version 2.0
  • 2013-10-14 Mon Release of version 1.1
  • 2013-09-01 Sun First release

Download

Version 2.0

Requirements

CANNOT INCLUDE FILE ../common/requirement1.org

How to use

scala -cp copris-puzzles-2.0.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-puzzles-2.0.jar sokoban.Solver -o opt input_file_name

If you have a SAT solver (such as MiniSat, GlueMiniSat) installed on your computer, you can use it to get better performance. Specify the full path of the SAT solver program with "-s1" or "-s2" option. 

scala -cp copris-puzzles-2.0.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-puzzles-2.0.jar sokoban.Solver -v -o opt data/m1-00001.txt
File = data/m1-00001.txt
Solver = 
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 2.0.

  • Copris solver was run on Intel Xeon 3.6Hz machine with:
    • Ubuntu Linux 20.04 (64 bit)
    • Java version "1.8.0_275", OpenJDK Runtime Environment (with "-Xmx2G" option)
    • Scala version 2.12.5
    • Copris version 2.3.1
    • Sugar version 2.3.4
  • GlueMiniSat version 2.2.10 (with preprocessing) is used as a SAT solver.

Finding a solution

  • We used 155 instances of Microban by David W. Skinner.
Number of instances
Solved within 3600s141
Timeout14
Error (Memory Over etc.)0
Total155
Avg. CPU time164.2
Max. CPU time3040.8

Source Code

The following shows the source code of the solver (Sokoban.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.

Links

Date: 2020-12-18 23:56:20 JST

Author: Naoyuki Tamura

Org version 7.8.02 with Emacs version 25

Validate XHTML 1.0