Hitori Solver in Copris

Table of Contents

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

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

Finding a solution

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)
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:  }

License

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

Links

?????

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

Author: Naoyuki Tamura

Org version 7.8.02 with Emacs version 23

Validate XHTML 1.0