Hitori Solver in Copris

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

This Hitori solver can find a solution of the given Hitori puzzle.

Version 2.0

• Scala jar file: ../build/copris-puzzles-2.0.jar (1575981 bytes)
• Source file: ../build/copris-puzzles-src-2.0.zip (29766 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.0.jar hitori.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.0.jar hitori.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.0.jar hitori.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 (Hitori.scala).

 1:  /*
 2:   * Hitori Solver in Copris
 3:   * by Naoyuki Tamura
 4:   * http://bach.istc.kobe-u.ac.jp/copris/puzzles/hitori/
 5:   */
 6:  package hitori
 7:  
 8:  import jp.kobe_u.copris._
 9:  import jp.kobe_u.copris.dsl._
10:  import puzzle._
11:  
12:  case class Hitori(m: Int, n: Int, board: Seq[Seq[String]]) extends BoardPuzzle {
13:    def show(sol: Set[Cell]) {
14:      for (i <- 0 until m) {
15:        for (j <- 0 until n) {
16:          val cell = (i,j)
17:          if (sol.contains(cell)) print("%3d".format(num(cell)))
18:          else print(" ##")
19:        }
20:        println
21:      }
22:    }
23:  }
24:  
25:  object Solver extends BoardPuzzleSolver[Hitori] {
26:    import scala.math.Ordering.Implicits._
27:  
28:    val name = "hitori.Solver"
29:    var whiteComponents: Set[Set[Cell]] = _
30:  
31:    def puzzleFactory(m: Int, n: Int, board: Seq[Seq[String]]) =
32:      Hitori(m, n, board)
33:  
34:    def define = {
35:      for (cell <- puzzle.cells)
36:        int('x(cell), Set(0, puzzle.num(cell)))
37:      for (i <- 0 until puzzle.m) {
38:        for (j1 <- 0 until puzzle.m; j2 <- j1+1 until puzzle.m; if puzzle.num((i,j1)) == puzzle.num((i,j2)))
39:          add(('x((i,j1)) === 0) || ('x((i,j2)) === 0))
40:      }
41:      for (j <- 0 until puzzle.n) {
42:        for (i1 <- 0 until puzzle.m; i2 <- i1+1 until puzzle.m; if puzzle.num((i1,j)) == puzzle.num((i2,j)))
43:          add(('x((i1,j)) === 0) || ('x((i2,j)) === 0))
44:      }
45:      for (cell <- puzzle.cells; cell1 <- puzzle.adjCells(cell))
46:        add(('x(cell) === 0) ==> ('x(cell1) > 0))
47:      // Hints
48:      if (puzzle.m >= 3 || puzzle.n >= 3) {
49:        for (cell <- puzzle.cells)
50:          add(('x(cell) > 0) ==> Or(puzzle.adjCells(cell).map(cell1 => 'x(cell1) > 0)))
51:      }
52:    }
53:  
54:    def checkSolution: Boolean = {
55:      val nodes = puzzle.cells.filter(cell => solution('x(cell)) > 0).toSet
56:      def nextCells(cell: Cell) =
57:        puzzle.adjCells(cell).filter(cell1 => solution('x(cell1)) > 0).toSet
58:      val arcs = nodes.map(cell => cell -> nextCells(cell)).toMap
59:      whiteComponents = getComponents(nodes, arcs)
60:      if (verbose >= 2)
61:        println("Components = " + whiteComponents.size)
62:      whiteComponents.size == 1
63:    }
64:    def addNegation {
65:      for (whites <- whiteComponents) {
66:        val blacks = for (cell <- whites; cell1 <- puzzle.adjCells(cell); if solution('x(cell1)) == 0)
67:                     yield cell1
68:        add(Or(whites.map(cell => 'x(cell) === 0)) || Or(blacks.map(cell => 'x(cell) > 0)))
69:      }
70:    }
71:    override def findFirstSolution = findIncremental(true, checkSolution, addNegation)
72:    override def findNextSolution = findIncremental(false, checkSolution, addNegation)
73:  
74:    def showSolution {
75:      require(whiteComponents.size == 1)
76:      val sol = whiteComponents.head
77:      if (quiet == 0) {
78:        println("Solution = " + sol)
79:        println("Size = " + sol.size)
80:        puzzle.show(sol)
81:      }
82:    }
83:  }

• It should be compiled with ../build/PuzzleSolver.scala.

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
• Hitori (by Nikoli)
• Wikipedia:Hitori
• http://www.janko.at/Raetsel/Hitori/