# 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

• 2013-10-14 Mon Release of version 1.1
• 2013-09-01 Sun First release

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-hitori-v1-1.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-hitori-v1-1.jar hitori.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-hitori-v1-1.jar hitori.Solver -o multi -s1 glucose 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-hitori-v1-0.jar hitori.Solver -v data/001.a.txt
BEGIN_solution = 1
Solution = Set((0,3), (1,1), (1,0), (1,2), (2,3), (2,0), (0,0), (2,2), (3,2), (3,1), (0,2))
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 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.

## Source Code

The following shows the source code of the solver (Hitori-v1-1.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:  }
``` 