Polarium Solver in Copris

Table of Contents

Overview

This page presents a Polarium solver written in Copris, a Constraint Programming DSL (Domain-Specific Language) embedded in Scala. Polarium is a puzzle game developed by Mitchell Corporation for the Nintendo DS game machine.

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

What's New

  • 2013-10-14 Mon Release of version 1.2
  • 2013-08-18 Sun Release of version 1.1
  • 2013-08-12 Mon Version number is added.
  • 2013-08-08 Thu First release

Download

Version 1.2
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-polarium-v1-2.jar polarium.Solver input_file_name
  • The format of the input file is explained below.

To find a solution with a minimum number of strokes, please use "-o opt" option ("-o min" option for version 1.0).

scala -cp copris-polarium-v1-2.jar polarium.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-polarium-v1-2.jar polarium.Solver -s1 glucose input_file_name

Input file format

The following is an example of input file.

7
7
+ + + + + + +
+ . * . * . +
+ . * . * . +
+ . * . * . +
+ . * . * . +
+ . * . * . +
+ + + + + + +
  • The first line gives the number of rows.
  • The second line gives the number of columns.
  • Borders are represented by "+".
  • Black cells are represented by "*".
  • White cells are represented by ".".

Example Usage

$ scala -cp copris-polarium-v1-1.jar polarium.Solver data/polarium-001.txt
BEGIN_solution = 1
Solution = List((1,4), (0,4), (0,3), (0,2), (1,2), (2,2), (3,2), (4,2), (5,2), (6,2), (6,3), (6,4), (5,4), (4,4), (3,4), (2,4))
Size = 16
+  +  +--+--+  +  +  
      |     |        
+  .  *  .  *  .  +  
      |              
+  .  *  .  *  .  +  
      |     |        
+  .  *  .  *  .  +  
      |     |        
+  .  *  .  *  .  +  
      |     |        
+  .  *  .  *  .  +  
      |     |        
+  +  +--+--+  +  +  
                     
END_solution = 1
NumOfSolutions >= 1
$ scala -cp copris-polarium-v1-1.jar polarium.Solver -o opt data/polarium-001.txt
BEGIN_solution = 1
Solution = List((1,4), (2,4), (3,4), (4,4), (5,4), (6,4), (6,3), (6,2), (5,2), (4,2), (3,2), (2,2), (1,2))
Size = 13
+  +  +  +  +  +  +  
                     
+  .  *  .  *  .  +  
      |     |        
+  .  *  .  *  .  +  
      |     |        
+  .  *  .  *  .  +  
      |     |        
+  .  *  .  *  .  +  
      |     |        
+  .  *  .  *  .  +  
      |     |        
+  +  +--+--+  +  +  
                     
END_solution = 1
NumOfOptSolutions >= 1

Performance Evaluation

Solver performance is measured on version 1.1.

  • Copris solver was run on Intel Xeon 3.47GHz machine with:
    • Ubuntu Linux 12.04 (32 bit)
    • Java version "1.6.0_27", OpenJDK Runtime Environment (with "-Xmx2G" 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

Finding a solution with a minimum number of strokes

Source Code

The following shows the source code of the solver (Polarium-v1-2.scala).

  1:  /*
  2:   * Polarium Solver in Copris
  3:   * by Naoyuki Tamura
  4:   * http://bach.istc.kobe-u.ac.jp/copris/puzzles/polarium/
  5:   */
  6:  package polarium
  7:  
  8:  import jp.kobe_u.copris._
  9:  import jp.kobe_u.copris.dsl._
 10:  import puzzle._
 11:  
 12:  case class Polarium(m: Int, n: Int, board: Seq[Seq[String]]) extends BoardPuzzle {
 13:    def isBorder(cell: Cell) = at(cell) == "+"
 14:    def isBlack(cell: Cell) = at(cell) == "*"
 15:    def isWhite(cell: Cell) = at(cell) == "."
 16:    val rows = 1 until m-1
 17:    def blacks(i: Int) = (0 until n).count(j => isBlack((i,j)))
 18:    def whites(i: Int) = (0 until n).count(j => isWhite((i,j)))
 19:    val minFlips = {
 20:      val flips = for (i <- rows) yield math.min(blacks(i), whites(i))
 21:      flips.sum
 22:    }
 23:    val maxFlips = {
 24:      val flips = for (i <- rows) yield math.max(blacks(i), whites(i))
 25:      val nodes = for (i <- 0 until m; j <- 0 until n) yield (i,j)
 26:      flips.sum + nodes.count(isBorder(_))
 27:    }
 28:    def show(sol: Seq[Cell]) {
 29:      val arcs = sol.sliding(2).map(e => (e(0),e(1))).toSet
 30:      def connected(cell1: Cell, cell2: Cell) =
 31:        arcs.contains((cell1,cell2)) || arcs.contains((cell2,cell1))
 32:      for (i <- 0 until m) {
 33:        for (j <- 0 until n) {
 34:          val cell = (i,j)
 35:          print(at(cell))
 36:          if (j+1 < n && connected(cell, (i,j+1))) print ("--")
 37:          else print ("  ")
 38:        }
 39:        println
 40:        for (j <- 0 until n) {
 41:          val cell = (i,j)
 42:          if (i+1 < m && connected(cell, (i+1,j))) print ("|  ")
 43:          else print ("   ")
 44:        }
 45:        println
 46:      }
 47:    }
 48:  }
 49:  
 50:  object Solver extends BoardPuzzleSolver[Polarium] {
 51:    import scala.math.Ordering.Implicits._
 52:  
 53:    val name = "polarium.Solver"
 54:  
 55:    def puzzleFactory(m: Int, n: Int, board: Seq[Seq[String]]) =
 56:      Polarium(m, n, board)
 57:  
 58:    def root = (puzzle.m,puzzle.n)
 59:    def cells = root +: puzzle.cells
 60:    def adjCells(cell: Cell) =
 61:      if (cell == root) puzzle.cells
 62:      else root +: puzzle.adjCells(cell)
 63:  
 64:    def define {
 65:      for (i <- puzzle.rows)
 66:        int('flip(i), 0, 1)
 67:      for (cell <- cells; cell1 <- adjCells(cell))
 68:        int('e(cell,cell1), 0, 1)
 69:      for (cell <- cells; cell1 <- adjCells(cell); if cell < cell1)
 70:        add('e(cell,cell1) + 'e(cell1,cell) <= 1)
 71:      for (cell <- cells) {
 72:        val in = adjCells(cell).map(cell1 => 'e(cell1,cell))
 73:        val ot = adjCells(cell).map(cell1 => 'e(cell,cell1))
 74:        int('io(cell), 0, 1)
 75:        add('io(cell) === Add(in))
 76:        add('io(cell) === Add(ot))
 77:        if (cell == root)
 78:          add('io(cell) === 1)
 79:        else if (puzzle.isBlack(cell))
 80:          add('flip(cell._1) === 'io(cell))
 81:        else if (puzzle.isWhite(cell))
 82:          add('flip(cell._1) =/= 'io(cell))
 83:      }
 84:      for (cell <- cells) {
 85:        int('x(cell), 0, puzzle.maxFlips)
 86:        for (cell1 <- adjCells(cell); if cell1 != root)
 87:          add(('e(cell,cell1) > 0) ==> ('x(cell) < 'x(cell1)))
 88:      }
 89:      if (options.contains("opt")) {
 90:        int('flips, puzzle.minFlips, puzzle.maxFlips)
 91:        minimize('flips)
 92:        for (cell <- cells)
 93:          add('x(cell) <= 'flips)
 94:        // Hints
 95:        val s = for (i <- puzzle.rows)
 96:          yield 'flip(i) * (puzzle.blacks(i) - puzzle.whites(i)) + puzzle.whites(i)
 97:        add(Add(s) <= 'flips)
 98:      }
 99:    }
100:  
101:    def showSolution {
102:      def path(cell: Cell): Seq[Cell] = {
103:        val cell1 = adjCells(cell).find(cell1 => solution('e(cell,cell1)) > 0).get
104:        if (cell1 == root) Seq.empty
105:        else cell1 +: path(cell1)
106:      }
107:      val sol = path(root)
108:      if (quiet == 0) {
109:        println("Solution = " + sol)
110:        println("Size = " + sol.size)
111:        puzzle.show(sol)
112:      }
113:    }
114:  }

License

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

Links

?????

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

Author: Naoyuki Tamura

Org version 7.8.02 with Emacs version 23

Validate XHTML 1.0