Nurikabe Solver in Copris

Table of Contents

Overview

This page presents a Nurikabe solver written in Copris, a Constraint Programming DSL (Domain-Specific Language) embedded in Scala. Nurikabe is a puzzle game developed by Nikoli.

This Nurikabe solver can find a solution of the given Nurikabe 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-nurikabe-v1-1.jar nurikabe.Solver input_file_name
  • The format of the input file is explained below.

To check the uniqueness of the solutions, please use "-o multi" option.

scala -cp copris-nurikabe-v1-1.jar nurikabe.Solver -o multi 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-nurikabe-v1-1.jar nurikabe.Solver -o multi -s1 glucose input_file_name

Input file format

The following is an example of input file.

10
10
- - - 1 - - - - - 2
- 1 - - - - - - - -
- - - - - - - - - -
- - - - - - - - - -
4 - - 1 - - - - - -
- - - - - - - - - -
- - - - - - - - - -
- - - - - - - - - -
7 - - - 11 - - - - -
- - 3 - - - 11 - - 5
  • The first line gives the number of rows.
  • The second line gives the number of columns.
  • Number cells are represented by its number.
  • Blank cells are represented by "-".

Example Usage

$ scala -cp copris-nurikabe-v1-0.jar nurikabe.Solver -v data/001.a.txt 
File = data/001.a.txt
Rows = 10
Cols = 10
Solver = 
Options = 
BEGIN_solution = 1
Solution = Set((4,2), (5,7), (3,4), (4,3), (4,9), (0,5), (3,3), (7,1), (3,5), (6,6), (3,7), (1,3), (7,8), (9,9), (5,0), (6,2), (1,2), (8,6), (9,0), (5,8), (2,5), (2,0), (5,9), (9,6), (2,1), (0,0), (4,6), (9,2), (2,9), (2,2), (0,1), (0,8), (3,8), (9,4), (1,7), (9,1), (1,6), (3,9), (0,9), (8,3), (7,5), (5,5), (6,3), (5,4), (2,7), (3,0), (5,6), (6,8), (7,6), (4,0), (5,3), (8,9), (8,7), (6,1), (9,5), (9,3), (8,8), (7,4), (1,9), (7,3), (0,2), (1,4), (4,1), (8,1), (1,5), (6,0))
Size = 66
## ## ## ..  2 ##  2 .. ## ## 
 2 .. ## ## ## ## ## ##  2 ## 
## ## ##  2 .. ## .. ## .. ## 
##  2 .. ## ## ##  2 ## ## ## 
## ## ## ## ..  2 ##  2 .. ## 
## ..  2 ## ## ## ## ## ## ## 
## ## ## ## ..  2 ##  2 ## .. 
.. ##  2 ## ## ## ## .. ##  2 
 2 ## .. ## ..  2 ## ## ## ## 
## ## ## ## ## ## ## ..  2 ## 

END_solution = 1
NumOfSolutions >= 1

Performance Evaluation

  • 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

Source Code

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

  1:  /*
  2:   * Nurikabe Solver in Copris
  3:   * by Naoyuki Tamura
  4:   * http://bach.istc.kobe-u.ac.jp/copris/puzzles/nurikabe/
  5:   */
  6:  package nurikabe
  7:  
  8:  import jp.kobe_u.copris._
  9:  import jp.kobe_u.copris.dsl._
 10:  import puzzle._
 11:  
 12:  case class Nurikabe(m: Int, n: Int, board: Seq[Seq[String]]) extends BoardPuzzle {
 13:    def isBlank(cell: Cell) = at(cell) == "-"
 14:    val numOfBlackCells = m * n - cells.filter(isNumber(_)).map(num(_)).sum
 15:    def show(sol: Set[Cell]) {
 16:      for (i <- 0 until m) {
 17:        for (j <- 0 until n) {
 18:          val cell = (i,j)
 19:          if (isNumber(cell)) print("%2d ".format(num(cell)))
 20:          else if (sol.contains(cell)) print("## ")
 21:          else print(".. ")
 22:        }
 23:        println
 24:      }
 25:      println
 26:    }
 27:  }
 28:  
 29:  object Solver extends BoardPuzzleSolver[Nurikabe] {
 30:    import scala.math.Ordering.Implicits._
 31:  
 32:    val name = "nurikabe.Solver"
 33:    var blackComponents: Set[Set[Cell]] = _
 34:  
 35:    def puzzleFactory(m: Int, n: Int, board: Seq[Seq[String]]) =
 36:      Nurikabe(m, n, board)
 37:  
 38:    def define = {
 39:      // Regions ('x(i,j): region index, 0 means black cell)
 40:      val regionMax = puzzle.numberCells.size
 41:      var regionIndex = 0
 42:      for (cell <- puzzle.cells) {
 43:        if (puzzle.isNumber(cell)) {
 44:          regionIndex += 1
 45:          int('x(cell), regionIndex)
 46:        } else {
 47:          int('x(cell), 0, regionMax)
 48:        }
 49:      }
 50:      // Black cells do not make 2x2 blocks
 51:      for ((i,j) <- puzzle.cells; if i < puzzle.m - 1 && j < puzzle.n - 1)
 52:        add(('x((i,j)) > 0) || ('x((i+1,j)) > 0) || ('x((i,j+1)) > 0) || ('x((i+1,j+1)) > 0))
 53:      // Different white regions are not connected
 54:      for ((i,j) <- puzzle.cells) {
 55:        if (i < puzzle.m - 1)
 56:          add((('x((i,j)) > 0) && ('x((i+1,j)) > 0)) ==> ('x((i,j)) === 'x((i+1,j))))
 57:        if (j < puzzle.n - 1)
 58:          add((('x((i,j)) > 0) && ('x((i,j+1)) > 0)) ==> ('x((i,j)) === 'x((i,j+1))))
 59:      }
 60:      // White region has specified size
 61:      // Construct a tree for each white region
 62:      for (cell <- puzzle.cells; cell1 <- puzzle.adjCells(cell)) {
 63:        int('e(cell,cell1), 0, 1)
 64:        add(('e(cell,cell1) === 1) ==> (('x(cell) > 0) && ('x(cell1) > 0)))
 65:      }
 66:      for (cell <- puzzle.cells; cell1 <- puzzle.adjCells(cell); if cell < cell1)
 67:        add('e(cell,cell1) + 'e(cell1,cell) <= 1)
 68:      for (cell <- puzzle.cells) {
 69:        val in = puzzle.adjCells(cell).map(cell1 => 'e(cell1,cell))
 70:        int('in(cell), 0, 1)
 71:        add('in(cell) === Add(in))
 72:        if (puzzle.isNumber(cell))
 73:          add('in(cell) === 0)
 74:        else
 75:          add(('x(cell) > 0) ==> ('in(cell) === 1))
 76:      }
 77:      // Count the size of each white region
 78:      val maxSize = puzzle.numberCells.map(cell => puzzle.num(cell)).max
 79:      for (cell <- puzzle.cells)
 80:        int('s(cell), 1, maxSize)
 81:      for (cell <- puzzle.cells) {
 82:        val s = for (cell1 <- puzzle.adjCells(cell))
 83:                yield If('e(cell,cell1) === 0, Num(0), 's(cell1))
 84:        add('s(cell) === Add(s) + 1)
 85:        if (puzzle.isNumber(cell))
 86:          add('s(cell) === puzzle.num(cell))
 87:      }
 88:      // Hints
 89:      for (cell <- puzzle.numberCells
 90:           if puzzle.num(cell) == 1; cell1 <- puzzle.adjCells(cell))
 91:        add('x(cell1) === 0)
 92:      for (cell <- puzzle.numberCells;
 93:           dij <- Seq((1,0), (0,1)); cell1 = puzzle.move(puzzle.move(cell, dij), dij)
 94:           if puzzle.isCell(cell1) && puzzle.isNumber(cell1))
 95:        add('x(puzzle.move(cell, dij)) === 0)
 96:      for (cell <- puzzle.numberCells;
 97:           dj <- Seq(-1, 1); cell1 = puzzle.move(cell, (1,dj))
 98:           if puzzle.isCell(cell1) && puzzle.isNumber(cell1)) {
 99:        add('x(puzzle.move(cell, (1,0))) === 0)
100:        add('x(puzzle.move(cell, (0,dj))) === 0)
101:      }
102:      if (puzzle.numOfBlackCells >= 2) {
103:        for (cell <- puzzle.cells; if puzzle.isBlank(cell))
104:          add(('x(cell) === 0) ==> Or(puzzle.adjCells(cell).map('x(_) === 0)))
105:      }
106:    }
107:  
108:    def checkSolution: Boolean = {
109:      val nodes = puzzle.cells.filter(cell => solution('x(cell)) == 0).toSet
110:      def nextCells(cell: Cell) =
111:        puzzle.adjCells(cell).filter(cell1 => solution('x(cell1)) == 0).toSet
112:      val arcs = nodes.map(cell => cell -> nextCells(cell)).toMap
113:      blackComponents = getComponents(nodes, arcs)
114:      if (verbose >= 2)
115:        println("Components = " + blackComponents.size)
116:      blackComponents.size == 1
117:    }
118:    def addNegation {
119:      for (blacks <- blackComponents) {
120:        val whites = for (cell <- blacks; cell1 <- puzzle.adjCells(cell); if solution('x(cell1)) > 0)
121:                     yield cell1
122:        add(Or(blacks.map(cell => 'x(cell) > 0)) || Or(whites.map(cell => 'x(cell) === 0)))
123:      }
124:    }
125:    override def findFirstSolution = findIncremental(true, checkSolution, addNegation)
126:    override def findNextSolution = findIncremental(false, checkSolution, addNegation)
127:  
128:    def showSolution {
129:      require(blackComponents.size == 1)
130:      val sol = blackComponents.head
131:      if (quiet == 0) {
132:        println("Solution = " + sol)
133:        println("Size = " + sol.size)
134:        puzzle.show(sol)
135:      }
136:    }
137:  }

License

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

Links

?????

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

Author: Naoyuki Tamura

Org version 7.8.02 with Emacs version 23

Validate XHTML 1.0