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

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

Download

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 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-puzzles-2.0.jar heyawake.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 heyawake.Solver -o multi -s2 minisat 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-puzzles-2.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((7,1), (7,5), (7,6), (1,5), (7,9), (5,0), (6,7), (0,0), (7,4), (5,1), (4,0), (3,4), (7,7), (0,9), (6,6), (3,1), (9,1), (6,1), (5,9), (6,2), (2,0), (0,3), (6,9), (4,4), (8,0), (1,6), (0,5), (6,5), (2,8), (6,8), (1,1), (6,3), (3,5), (4,6), (8,3), (9,8), (1,9), (2,6), (8,2), (0,8), (8,8), (4,9), (0,4), (2,9), (5,7), (5,4), (3,2), (1,3), (2,2), (5,5), (4,8), (4,2), (2,4), (3,7), (0,1), (9,6), (5,3), (1,7), (2,3), (1,2), (4,3), (9,9), (8,7), (8,5), (9,4), (7,2), (9,5), (1,0), (3,8), (5,6), (0,6), (9,2), (7,0))
Size = 73
 .. .. ## .. .. .. .. ## .. ..
 .. .. .. .. ## .. .. .. ## ..
 .. ## .. .. .. ## .. ## .. ..
 ## .. .. ## .. .. ## .. .. ##
 .. ## .. .. .. ## .. ## .. ..
 .. .. ## .. .. .. .. .. ## ..
 ## .. .. .. ## .. .. .. .. ..
 .. .. .. ## .. .. .. .. ## ..
 .. ## .. .. ## .. ## .. .. ##
 ## .. .. ## .. .. .. ## .. ..
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 3600s370
Timeout0
Error (Memory Over etc.)0
Total370
Avg. CPU time6.2
Max. CPU time174.1

Source Code

The following shows the source code of the solver (Heyawake.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 ../build/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.

Links

Date: 2020-12-18 23:55:57 JST

Author: Naoyuki Tamura

Org version 7.8.02 with Emacs version 25

Validate XHTML 1.0