Masyu Solver in Copris

Table of Contents

Overview

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

This Masyu solver can find a solution of the given Masyu puzzle.

What's New

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

Download

Version 1.0
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-masyu-v1-1.jar masyu.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-masyu-v1-1.jar masyu.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-masyu-v1-1.jar masyu.Solver -o multi -s1 glucose input_file_name

Input file format

The following is an example of input file.

6
6
- - w - - -
w - - - - b
- - - - - -
- - - - - -
b - - - - w
- - - w - -
  • The first line gives the number of rows.
  • The second line gives the number of columns.
  • Black dot cells are represented by "b".
  • White dot cells are represented by "w".
  • Blank cells are represented by "-".

Example Usage

$ scala -cp copris-masyu-v1-0.jar masyu.Solver -v data/001.a.txt 
File = data/001.a.txt
Rows = 6
Cols = 6
Solver = 
Options = 
BEGIN_solution = 1
Solution = List((0,3), (0,2), (0,1), (0,0), (1,0), (2,0), (3,0), (4,0), (4,1), (4,2), (5,2), (5,3), (5,4), (5,5), (4,5), (3,5), (2,5), (1,5), (1,4), (1,3), (0,3))
Size = 21
 .   .   .   .   .   .   .
   +---+---w---+   +   +  
 . | .   .   . | .   .   .
   w   +   +   +---+---b  
 . | .   .   .   .   . | .
   +   +   +   +   +   +  
 . | .   .   .   .   . | .
   +   +   +   +   +   +  
 . | .   .   .   .   . | .
   b---+---+   +   +   w  
 .   .   . | .   .   . | .
   +   +   +---w---+---+  
 .   .   .   .   .   .   .
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 (Masyu-v1-1.scala).

  1:  /*
  2:   * Masyu Solver in Copris
  3:   * by Naoyuki Tamura
  4:   * http://bach.istc.kobe-u.ac.jp/copris/puzzles/masyu/
  5:   */
  6:  package masyu
  7:  
  8:  import jp.kobe_u.copris._
  9:  import jp.kobe_u.copris.dsl._
 10:  import puzzle._
 11:  
 12:  case class Masyu(m: Int, n: Int, board: Seq[Seq[String]]) extends BoardPuzzle {
 13:    def isWhite(cell: Cell) = at(cell) == "w"
 14:    def isBlack(cell: Cell) = at(cell) == "b"
 15:    def isBlank(cell: Cell) = at(cell) == "-"
 16:    def adj2(cell: Cell) = {
 17:      val (i,j) = cell
 18:      for ((di,dj) <- dijs; if isCell((i+di,j+dj)) && isCell((i-di,j-dj)))
 19:      yield ((i+di,j+dj), (i-di,j-dj))
 20:    }
 21:    def show(sol: Seq[Cell]) {
 22:      val arcs = sol.sliding(2).map(e => (e(0),e(1))).toSet
 23:      def connected(cell1: Cell, cell2: Cell) =
 24:        arcs.contains((cell1,cell2)) || arcs.contains((cell2,cell1))
 25:      for (i <- 0 until m) {
 26:        print(" .")
 27:        for (j <- 0 until n) {
 28:          val cell = (i,j); val cell1 = (i-1,j)
 29:          if (isCell(cell1) && connected(cell, cell1)) print(" | .")
 30:          else print("   .")
 31:        }
 32:        println
 33:        if (i < m) {
 34:          for (j <- 0 until n) {
 35:          val cell = (i,j); val cell1 = (i,j-1)
 36:            if (isCell(cell1) && connected(cell, cell1)) print("---")
 37:            else print("   ")
 38:            if (isBlank(cell)) print("+")
 39:            else print(at(cell))
 40:          }
 41:          println("  ")
 42:        }
 43:      }
 44:      println(" ." + "   ." * n)
 45:    }
 46:  }
 47:  
 48:  object Solver extends BoardPuzzleSolver[Masyu] {
 49:    import scala.math.Ordering.Implicits._
 50:  
 51:    val name = "masyu.Solver"
 52:    var cycles: Set[Seq[Cell]] = _
 53:  
 54:    def puzzleFactory(m: Int, n: Int, board: Seq[Seq[String]]) =
 55:      Masyu(m, n, board)
 56:  
 57:    def define = {
 58:      for (cell <- puzzle.cells; cell1 <- puzzle.adjCells(cell))
 59:        int('e(cell,cell1), 0, 1)
 60:      for (cell <- puzzle.cells; cell1 <- puzzle.adjCells(cell); if cell < cell1)
 61:        add('e(cell,cell1) + 'e(cell1,cell) <= 1)
 62:      for (cell <- puzzle.cells) {
 63:        val in = puzzle.adjCells(cell).map(cell1 => 'e(cell1,cell))
 64:        val ot = puzzle.adjCells(cell).map(cell1 => 'e(cell,cell1))
 65:        int('io(cell), 0, 1)
 66:        add('io(cell) === Add(in))
 67:        add('io(cell) === Add(ot))
 68:        if (puzzle.isWhite(cell) || puzzle.isBlack(cell))
 69:          add('io(cell) === 1)
 70:      }
 71:      // Straight line
 72:      for (cell <- puzzle.cells) {
 73:        int('s(cell), 0, 1)
 74:        val s = for ((cell1,cell2) <- puzzle.adj2(cell))
 75:                yield ('e(cell1,cell) === 1) && ('e(cell,cell2) === 1)
 76:        add(('s(cell) === 1) <==> Or(s))
 77:      }
 78:      for (cell <- puzzle.cells) {
 79:        if (puzzle.isWhite(cell)) {
 80:          add('s(cell) === 1)
 81:          for ((cell1,cell2) <- puzzle.adj2(cell))
 82:            add((('e(cell1,cell) === 1) || ('e(cell,cell1) === 1)) ==>
 83:                (('s(cell1) === 0) || ('s(cell2) === 0)))
 84:        } else if (puzzle.isBlack(cell)) {
 85:          add('s(cell) === 0)
 86:          for (cell1 <- puzzle.adjCells(cell))
 87:            add((('e(cell1,cell) === 1) || ('e(cell,cell1) === 1)) ==>
 88:                ('s(cell1) === 1))
 89:        }
 90:      }
 91:    }
 92:  
 93:    def checkSolution: Boolean = {
 94:      val nodes = puzzle.cells.filter(cell => solution('io(cell)) > 0).toSet
 95:      def nextCells(cell: Cell) =
 96:        puzzle.adjCells(cell).filter(cell1 => solution('e(cell,cell1)) > 0).toSet
 97:      val arcs = nodes.map(cell => cell -> nextCells(cell)).toMap
 98:      cycles = getCycles(nodes, arcs)
 99:      cycles = cycles.filter(cycle => cycle.exists(cell => ! puzzle.isBlank(cell)))
100:      if (verbose >= 2)
101:        println("Cycles = " + cycles.size)
102:      cycles.size == 1
103:    }
104:    def addNegation {
105:      for (cycle <- cycles) {
106:        add(Or(cycle.sliding(2).map(e => 'e(e(0),e(1)) === 0).toSeq))
107:        add(Or(cycle.reverse.sliding(2).map(e => 'e(e(0),e(1)) === 0).toSeq))
108:      }
109:    }
110:    override def findFirstSolution = findIncremental(true, checkSolution, addNegation)
111:    override def findNextSolution = findIncremental(false, checkSolution, addNegation)
112:  
113:    def showSolution {
114:      // Cycle
115:      require(cycles.size == 1)
116:      val sol = cycles.head
117:      if (quiet == 0) {
118:        println("Solution = " + sol)
119:        println("Size = " + sol.size)
120:        puzzle.show(sol)
121:      }
122:    }
123:  }

License

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

Links

?????

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

Author: Naoyuki Tamura

Org version 7.8.02 with Emacs version 23

Validate XHTML 1.0