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

  • 2020-12-15 Tue Release of version 2.0
  • 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 2.0

Requirements

  • Scala version 2.12 to be installed
    • Other Scala version is not binary compatible with version 2.12.
  • Copris (included in the package)
  • Sugar (included in the package)
  • Sat4j Core (included in the package)

How to use

scala -cp copris-puzzles-2.0.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

scala -cp copris-puzzles-2.0.jar polarium.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 polarium.Solver -o opt -s2 minisat 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-puzzles-2.0.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-puzzles-2.0.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 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

Number of instances
Solved within 3600s100
Timeout0
Error (Memory Over etc.)0
Total100
Avg. CPU time3.1
Max. CPU time4.5

Source Code

The following shows the source code of the solver (Polarium-.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 (cell <- cells; cell1 <- adjCells(cell); if cell1 != root)
 87:        add(('e(cell,cell1) > 0) ==> ('x(cell) < 'x(cell1)))
 88:      if (options.contains("opt")) {
 89:        int('flips, puzzle.minFlips, puzzle.maxFlips)
 90:        minimize('flips)
 91:        for (cell <- cells)
 92:          add('x(cell) <= 'flips)
 93:        // Hints
 94:        val s = for (i <- puzzle.rows)
 95:          yield 'flip(i) * (puzzle.blacks(i) - puzzle.whites(i)) + puzzle.whites(i)
 96:        add(Add(s) <= 'flips)
 97:      }
 98:    }
 99:  
100:    def showSolution {
101:      def path(cell: Cell): Seq[Cell] = {
102:        val cell1 = adjCells(cell).find(cell1 => solution('e(cell,cell1)) > 0).get
103:        if (cell1 == root) Seq.empty
104:        else cell1 +: path(cell1)
105:      }
106:      val sol = path(root)
107:      if (quiet == 0) {
108:        println("Solution = " + sol)
109:        println("Size = " + sol.size)
110:        puzzle.show(sol)
111:      }
112:    }
113:  }

License

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

Links

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

Author: Naoyuki Tamura

Org version 7.8.02 with Emacs version 25

Validate XHTML 1.0