Shikaku Solver in Copris

Table of Contents

Overview

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

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

Input file format

The following is an example of input file.

10
10
- 4 - - - 2 - - - 3
3 - - - 5 - - - 3 -
- - - 3 - - - 6 - -
- - 3 - - - 5 - - -
- 3 - - - 4 - - - 5
2 - - - 7 - - - 3 -
- - - 5 - - - 4 - -
- - 5 - - - 4 - - -
- 6 - - - 2 - - - 3
2 - - - 5 - - - 3 -
  • The first line gives the number of rows.
  • The second line gives the number of columns.
  • Number cells are represented by its number.
  • Blank cells are represented by "-".

Example Usage

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

 1:  /*
 2:   * Shikaku Solver in Copris
 3:   * by Naoyuki Tamura
 4:   * http://bach.istc.kobe-u.ac.jp/copris/puzzles/shikaku/
 5:   */
 6:  package shikaku
 7:  
 8:  import jp.kobe_u.copris._
 9:  import jp.kobe_u.copris.dsl._
10:  import puzzle._
11:  
12:  case class Shikaku(m: Int, n: Int, board: Seq[Seq[String]]) extends BoardPuzzle {
13:    def isBlank(cell: Cell) = at(cell) == "-"
14:    def sizes(cell: Cell) = {
15:      val a = num(cell)
16:      for (h <- 1 to a; if a % h == 0) yield (h, a / h)
17:    }
18:    def show(sol: Seq[(Cell,(Int,Int))]) {
19:      val map = (
20:        for {
21:          k <- 0 until sol.size
22:          ((r,c),(h,w)) = sol(k)
23:          i <- r until r+h; j <- c until c+w
24:        } yield (i,j) -> k
25:      ).toMap
26:      def s(i: Int, j: Int) = map.getOrElse((i,j), -1)
27:      for (i <- 0 to m) {
28:        for (j <- 0 until n) {
29:          print("+")
30:          if (s(i,j) != s(i-1,j)) print("---")
31:          else print("   ")
32:        }
33:        println("+")
34:        if (i < m) {
35:          for (j <- 0 until n) {
36:            if (s(i,j) != s(i,j-1)) print("|")
37:            else print(" ")
38:            if (isNumber(i, j)) print("%3d".format(num(i, j)))
39:            else print("   ")
40:          }
41:          println("|")
42:        }
43:      }
44:    }
45:  }
46:  
47:  object Solver extends BoardPuzzleSolver[Shikaku] {
48:    val name = "shikaku.Solver"
49:  
50:    def puzzleFactory(m: Int, n: Int, board: Seq[Seq[String]]) =
51:      Shikaku(m, n, board)
52:  
53:    def define = {
54:      for (k <- 0 until puzzle.numberCells.size; cell = puzzle.numberCells(k)) {
55:        int('r(k), 0, puzzle.m-1)
56:        int('c(k), 0, puzzle.n-1)
57:        int('h(k), puzzle.sizes(cell).map(_._1).toSet)
58:        int('w(k), puzzle.sizes(cell).map(_._2).toSet)
59:        for ((h,w) <- puzzle.sizes(cell))
60:          add(('h(k) === h) <==> ('w(k) === w))
61:        add('r(k) + 'h(k) <= puzzle.m)
62:        add('c(k) + 'w(k) <= puzzle.n)
63:        val (i,j) = cell
64:        add(('r(k) <= i) && ('r(k) + 'h(k) > i))
65:        add(('c(k) <= j) && ('c(k) + 'w(k) > j))
66:      }
67:      for (k1 <- 0 until puzzle.numberCells.size; k2 <- k1+1 until puzzle.numberCells.size)
68:        add(('r(k1) + 'h(k1) <= 'r(k2)) || ('r(k2) + 'h(k2) <= 'r(k1)) || 
69:            ('c(k1) + 'w(k1) <= 'c(k2)) || ('c(k2) + 'w(k2) <= 'c(k1)))
70:    }
71:  
72:    def showSolution {
73:      val sol = for (k <- 0 until puzzle.numberCells.size)
74:                yield ((solution('r(k)),solution('c(k))), (solution('h(k)),solution('w(k))))
75:      if (quiet == 0) {
76:        println("Solution = " + sol)
77:        println("Size = " + sol.size)
78:        puzzle.show(sol)
79:      }
80:    }
81:  }

License

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

Links

?????

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

Author: Naoyuki Tamura

Org version 7.8.02 with Emacs version 23

Validate XHTML 1.0