Yajilin Solver in Copris

Table of Contents

Overview

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

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

Input file format

The following is an example of input file.

7
7
- 1w  -  -  -  -  -
-  -  - 0e  -  -  -
-  -  -  -  - 1e  -
- 1w  - 2s  -  -  -
-  -  -  -  -  -  -
-  -  -  -  - 1w  -
-  -  -  -  -  -  -
  • The first line gives the number of rows.
  • The second line gives the number of columns.
  • Blank cells are represented by "-".
  • Arrow cells are represented by the number followed by the direction (n, s, e, w).

Example Usage

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

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

License

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

Links

?????

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

Author: Naoyuki Tamura

Org version 7.8.02 with Emacs version 23

Validate XHTML 1.0