Kurodoko Solver in Copris

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.

Version 2.1

• Scala jar file: ../build/copris-puzzles-2.1.jar (1576060 bytes)
• Source file: ../build/copris-puzzles-src-2.1.zip (29777 bytes)

• 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)

scala -cp copris-puzzles-2.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-puzzles-2.1.jar kurodoko.Solver -o multi 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.1.jar kurodoko.Solver -o multi -s2 minisat input_file_name

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.

The following shows the source code of the solver (Kurodoko.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)) || Or(whites.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 ../build/PuzzleSolver.scala.
• We assume the maximum size of polyomions not appeared as hints does not exceed 20.

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

• Copris (Constraint Programming DSL embedded in Scala)
• Sugar (an award winning Constraint Solver)
  • Default constraint solver used in Copris
• Sat4j (SAT solver in Java)
  • Default SAT solver used in Copris
• Kurodoko (by Nikoli)
• Wikipedia:Kuromasu
• http://www.janko.at/Raetsel/Kuromasu/