Kurodoko Solver in Copris

Table of Contents

Overview

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

This Kurodoko solver can find a solution of the given Kurodoko 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-kurodoko-v1-1.jar kurodoko.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-kurodoko-v1-1.jar kurodoko.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-kurodoko-v1-1.jar kurodoko.Solver -o multi -s1 glucose input_file_name

Input file format

The following is an example of input file.

9
9
9 - - 8 - 9 - 8 -
- - - - - - 9 - -
- - - - - - - 3 -
3 - - - - 4 - - 3
- - 4 - - - 9 - -
4 - - 6 - - - - 4
- 15 - - - - - - -
- - 7 - - - - - -
- 7 - 5 - 4 - - 4
  • 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-kurodoko-v1-0.jar kurodoko.Solver -v data/001.a.txt
File = data/001.a.txt
Solver = 
Options = 
Rows = 9
Cols = 9
BEGIN_solution = 1
Solution = Vector(Vector(0, 0, 0, 0, 0, 0, 0, 0, 1), Vector(0, 1, 0, 1, 0, 0, 0, 1, 0), Vector(1, 0, 1, 0, 0, 1, 0, 0, 0), Vector(0, 0, 0, 1, 0, 0, 0, 1, 0), Vector(1, 0, 0, 0, 1, 0, 0, 0, 1), Vector(0, 0, 1, 0, 0, 1, 0, 1, 0), Vector(0, 0, 0, 0, 0, 0, 0, 0, 0), Vector(0, 0, 0, 0, 0, 0, 1, 0, 0), Vector(1, 0, 1, 0, 1, 0, 0, 1, 0))
Size = 9
  9 .. ..  8 ..  9 ..  8 ##
 .. ## .. ## .. ..  9 ## ..
 ## .. ## .. .. ## ..  3 ..
  3 .. .. ## ..  4 .. ##  3
 ## ..  4 .. ## ..  9 .. ##
  4 .. ##  6 .. ## .. ##  4
 .. 15 .. .. .. .. .. .. ..
 .. ..  7 .. .. .. ## .. ..
 ##  7 ##  5 ##  4 .. ##  4
END_solution = 1
NumOfSolutions >= 1

Performance Evaluation

Solver performance is measured on version 1.0.

  • 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 (Kurodoko-v1-1.scala).

 1:  /*
 2:   * Kurodoko Solver in Copris
 3:   * by Naoyuki Tamura
 4:   * http://bach.istc.kobe-u.ac.jp/copris/puzzles/kurodoko/
 5:   */
 6:  package kurodoko
 7:  
 8:  import jp.kobe_u.copris._
 9:  import jp.kobe_u.copris.dsl._
10:  import puzzle._
11:  
12:  case class Kurodoko(m: Int, n: Int, board: Seq[Seq[String]]) extends BoardPuzzle {
13:    def show(sol: Seq[Seq[Int]]) {
14:      for (i <- 0 until m) {
15:        for (j <- 0 until n) {
16:          val cell = (i,j)
17:          if (isNumber(cell)) print("%3d".format(num(cell)))
18:          else if (sol(i)(j) == 0) print(" ..")
19:          else print(" ##")
20:        }
21:        println
22:      }
23:    }
24:  }
25:  
26:  object Solver extends BoardPuzzleSolver[Kurodoko] {
27:    import scala.math.Ordering.Implicits._
28:  
29:    val name = "kurodoko.Solver"
30:    var whiteComponents: Set[Set[Cell]] = _
31:  
32:    def puzzleFactory(m: Int, n: Int, board: Seq[Seq[String]]) =
33:      Kurodoko(m, n, board)
34:  
35:    def define = {
36:      for (cell <- puzzle.cells) {
37:        // 'x(cell): = 0 white, = 1 black
38:        if (puzzle.isNumber(cell))
39:          int('x(cell), 0)
40:        else
41:          int('x(cell), 0, 1)
42:        for (dij <- puzzle.dijs) {
43:          // 'c(cell, dij); the number of white cells from cell to dij
44:          int('c(cell,dij), 0, math.max(puzzle.m, puzzle.n))
45:        }
46:      }
47:      for (cell <- puzzle.cells; cell1 <- puzzle.adjCells(cell); if cell < cell1)
48:        add(('x(cell) === 0) || ('x(cell1) === 0))
49:      for (cell <- puzzle.cells; dij <- puzzle.dijs) {
50:        add(('x(cell) > 0) ==> ('c(cell,dij) === 0))
51:        val cell1 = puzzle.move(cell, dij)
52:        if (puzzle.isCell(cell1))
53:          add(('x(cell) === 0) ==> ('c(cell,dij) === 'c(cell1,dij) + 1))
54:        else
55:          add(('x(cell) === 0) ==> ('c(cell,dij) === 1))
56:      }
57:      for (cell <- puzzle.cells; if puzzle.isNumber(cell)) {
58:        val s = for (dij <- puzzle.dijs) yield 'c(cell,dij)
59:        add(Add(s) - 3 === puzzle.num(cell))
60:      }
61:    }
62:  
63:    def checkSolution: Boolean = {
64:      val nodes = puzzle.cells.filter(cell => solution('x(cell)) == 0).toSet
65:      def nextCells(cell: Cell) =
66:        puzzle.adjCells(cell).filter(cell1 => solution('x(cell1)) == 0).toSet
67:      val arcs = nodes.map(cell => cell -> nextCells(cell)).toMap
68:      whiteComponents = getComponents(nodes, arcs)
69:      if (verbose >= 2)
70:        println("Components = " + whiteComponents.size)
71:      whiteComponents.size == 1
72:    }
73:    def addNegation {
74:      for (whites <- whiteComponents) {
75:        val blacks = for (cell <- whites; cell1 <- puzzle.adjCells(cell); if solution('x(cell1)) > 0)
76:                     yield cell1
77:        add(Or(blacks.map(cell => 'x(cell) === 0)))
78:      }
79:    }
80:    override def findFirstSolution = findIncremental(true, checkSolution, addNegation)
81:    override def findNextSolution = findIncremental(false, checkSolution, addNegation)
82:  
83:    def showSolution {
84:      val sol = for (i <- 0 until puzzle.m)
85:                yield (0 until puzzle.n).map(j => solution('x((i,j))))
86:      if (quiet == 0) {
87:        println("Solution = " + sol)
88:        println("Size = " + sol.size)
89:        puzzle.show(sol)
90:      }
91:    }
92:  }
  • It should be compiled with PuzzleSolver.scala.
  • We assume the maximum size of polyomions not appeared as hints does not exceed 20.

License

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

Links

?????

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

Author: Naoyuki Tamura

Org version 7.8.02 with Emacs version 23

Validate XHTML 1.0