Heyawake Solver in Copris

Table of Contents

Overview

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

This Heyawake solver can find a solution of the given Heyawake 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-heyawake-v1-1.jar heyawake.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-heyawake-v1-1.jar heyawake.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-heyawake-v1-1.jar heyawake.Solver -o multi -s1 glucose input_file_name

Input file format

The following is an example of input file.

10
10
a a:1 a b b c c d:1 e e
a a a b b c c d e e
f:3 f g g g h:5 h h i i
f f g g g h h h i i
f f g g g h h h j j
k k l l l m:0 m m n n
o o l l l m m m n n
o o l l l m m m n n
p:2 p q r:2 r s s t t t
p p q r r s s t t t
  • The first line gives the number of rows.
  • The second line gives the number of columns.
  • Each region is specified by its name.
  • The number after the region name specifies the number of black cells in the region.

Example Usage

$ scala -cp copris-heyawake-v1-0.jar heyawake.Solver -v data/001.a.txt
File = data/001.a.txt
Solver = 
Options = 
Rows = 10
Cols = 10
BEGIN_solution = 1
Solution = Set((0,3), (4,2), (5,7), (3,4), (4,3), (4,9), (1,1), (7,2), (0,5), (8,5), (0,4), (7,1), (3,5), (6,6), (7,9), (3,7), (1,3), (2,8), (9,9), (6,5), (5,0), (1,0), (6,2), (2,6), (1,2), (2,3), (2,4), (5,1), (2,0), (5,9), (9,6), (0,0), (4,6), (6,7), (9,2), (2,9), (2,2), (0,1), (0,8), (3,8), (9,4), (1,7), (9,1), (1,6), (4,4), (0,9), (8,3), (6,9), (9,8), (7,5), (5,5), (6,3), (5,4), (3,2), (7,7), (5,6), (6,8), (7,0), (7,6), (4,0), (5,3), (8,2), (8,7), (6,1), (0,6), (9,5), (8,8), (7,4), (3,1), (1,9), (8,0), (4,8), (1,5))
Size = 73
 .. .. ## .. .. .. .. ## .. ..
 .. .. .. .. ## .. .. .. ## ..
 .. ## .. .. .. ## .. ## .. ..
 ## .. .. ## .. .. ## .. .. ##
 .. ## .. .. .. ## .. ## .. ..
 .. .. ## .. .. .. .. .. ## ..
 ## .. .. .. ## .. .. .. .. ..
 .. .. .. ## .. .. .. .. ## ..
 .. ## .. .. ## .. ## .. .. ##
 ## .. .. ## .. .. .. ## .. ..
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 (Heyawake-v1-1.scala).

 1:  /*
 2:   * Heyawake Solver in Copris
 3:   * by Naoyuki Tamura
 4:   * http://bach.istc.kobe-u.ac.jp/copris/puzzles/heyawake/
 5:   */
 6:  package heyawake
 7:  
 8:  import jp.kobe_u.copris._
 9:  import jp.kobe_u.copris.dsl._
10:  import puzzle._
11:  
12:  case class Heyawake(m: Int, n: Int, board: Seq[Seq[String]]) extends BoardPuzzle {
13:    def areaName(cell: Cell) = at(cell).split(":")(0)
14:    val areaNames = cells.map(areaName).toSet
15:    val areaSize = {
16:      for (cell <- cells; if at(cell).contains(":"))
17:      yield areaName(cell) -> at(cell).split(":")(1).toInt
18:    }.toMap
19:    val areaCells =
20:      areaNames.map(name => name -> cells.filter(cell => areaName(cell) == name).toSet).toMap
21:    val badBlocks: Seq[Seq[Cell]] = {
22:      def findBlock(cell: Cell, dij: Cell, name: String, block0: Seq[Cell]): Option[Seq[Cell]] =
23:        if (! isCell(cell)) None
24:        else if (areaName(cell) != name) Some((cell +: block0).reverse)
25:        else findBlock(move(cell, dij), dij, name, cell +: block0)
26:      for {
27:        dij <- Seq((0,1), (1,0)); i <- 0 until m; j <- 0 until n
28:        cell = (i,j); cell1 = move(cell, dij)
29:        if isCell(cell1) && areaName(cell) != areaName(cell1)
30:        block <- findBlock(cell1, dij, areaName(cell1), Seq(cell))
31:      } yield block
32:    }
33:    def show(sol: Set[Cell]) {
34:      for (i <- 0 until m) {
35:        for (j <- 0 until n)
36:          if (sol.contains((i,j))) print(" ..")
37:          else print(" ##")
38:        println
39:      }
40:    }
41:  }
42:  
43:  object Solver extends BoardPuzzleSolver[Heyawake] {
44:    import scala.math.Ordering.Implicits._
45:  
46:    val name = "heyawake.Solver"
47:    var whiteComponents: Set[Set[Cell]] = _
48:  
49:    def puzzleFactory(m: Int, n: Int, board: Seq[Seq[String]]) =
50:      Heyawake(m, n, board)
51:  
52:    def define = {
53:      for (cell <- puzzle.cells)
54:        int('x(cell), 0, 1)
55:      for (cell <- puzzle.cells; cell1 <- puzzle.adjCells(cell); if cell < cell1)
56:        add(('x(cell) === 0) || ('x(cell1) === 0))
57:      for (area <- puzzle.areaNames)
58:        if (puzzle.areaSize.contains(area)) {
59:          val xs = puzzle.areaCells(area).map(cell => 'x(cell))
60:          add(Add(xs) === puzzle.areaSize(area))
61:        }
62:      for (block <- puzzle.badBlocks)
63:        add(Or(block.map(cell => 'x(cell) =/= 0)))
64:      if (puzzle.m >= 3 || puzzle.n >= 3) {
65:        for (cell <- puzzle.cells)
66:          add(('x(cell) === 0) ==> Or(puzzle.adjCells(cell).map(cell1 => 'x(cell1) === 0)))
67:      }
68:    }
69:  
70:    def checkSolution: Boolean = {
71:      val nodes = puzzle.cells.filter(cell => solution('x(cell)) == 0).toSet
72:      def nextCells(cell: Cell) =
73:        puzzle.adjCells(cell).filter(cell1 => solution('x(cell1)) == 0).toSet
74:      val arcs = nodes.map(cell => cell -> nextCells(cell)).toMap
75:      whiteComponents = getComponents(nodes, arcs)
76:      if (verbose >= 2)
77:        println("Components = " + whiteComponents.size)
78:      whiteComponents.size == 1
79:    }
80:    def addNegation {
81:      for (whites <- whiteComponents) {
82:        val blacks = for (cell <- whites; cell1 <- puzzle.adjCells(cell); if solution('x(cell1)) > 0)
83:                     yield cell1
84:        add(Or(whites.map(cell => 'x(cell) > 0)) || Or(blacks.map(cell => 'x(cell) === 0)))
85:      }
86:    }
87:    override def findFirstSolution = findIncremental(true, checkSolution, addNegation)
88:    override def findNextSolution = findIncremental(false, checkSolution, addNegation)
89:  
90:    def showSolution {
91:      val sol = puzzle.cells.filter(cell => solution('x(cell)) == 0).toSet
92:      if (quiet == 0) {
93:        println("Solution = " + sol)
94:        println("Size = " + sol.size)
95:        puzzle.show(sol)
96:      }
97:    }
98:  }
  • It should be compiled with PuzzleSolver.scala.
  • We assume the maximum size of polyomions not appeared as hints does not exceed 20.

License

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

Links

?????

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

Author: Naoyuki Tamura

Org version 7.8.02 with Emacs version 23

Validate XHTML 1.0