Hitori Solver in Copris

Overview

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.

What's New

• 2020-12-15 Tue Release of version 2.0
• 2013-10-14 Mon Release of version 1.1
• 2013-09-01 Sun First release

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 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
```

Input file format

The following is an example of input file.

```4
4
3 3 1 4
4 3 2 2
1 3 4 2
3 4 3 2
```
• The first line gives the number of rows.
• The second line gives the number of columns.
• Number cells are represented by its number.

Example Usage

```\$ scala -cp copris-puzzles-2.0.jar hitori.Solver -v data/001.a.txt
File = data/001.a.txt
Solver =
Options =
Rows = 4
Cols = 4
BEGIN_solution = 1
Solution = Set((0,2), (0,0), (3,1), (2,0), (0,3), (1,1), (3,2), (2,2), (2,3), (1,2), (1,0))
Size = 11
3 ##  1  4
4  3  2 ##
1 ##  4  2
##  4  3 ##
END_solution = 1
NumOfSolutions >= 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 3600s659
Timeout0
Error (Memory Over etc.)0
Total659
Avg. CPU time2.8
Max. CPU time41.4

Source Code

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)
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:    }
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)
77:      if (quiet == 0) {
78:        println("Solution = " + sol)
79:        println("Size = " + sol.size)
80:        puzzle.show(sol)
81:      }
82:    }
83:  }
```