Nonogram Solver in Copris

Table of Contents

Overview

This page presents a Nonogram solver written in Copris, a Constraint Programming DSL (Domain-Specific Language) embedded in Scala. It can solve a very large puzzle, such as Warship (100 x 100) by P. R. H. Ainsworth available from http://www.comp.lancs.ac.uk/~ss/nonogram/puzzles.

What's New

  • 2013-10-14 Mon Release of version 1.2
  • 2013-08-12 Mon Version number is added.
  • 2013-04-16 Tue "N-Dom Puzzles" section is added.
  • 2013-04-08 Mon "Constraint Model" section is added.
  • 2013-02-16 Sat First release

Download

Version 1.2
Version 1.1
Version 1.0
Multicolor version

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-nonogram-v1-2.jar nonogram.Solver cwd_file_name
  • CWD format file can be read by the solver.
  • Visit Web Paint-by-Number Puzzle Export page by Jan Wolter to download CWD format files.
  • The program also checks the uniqueness of the solution.

For some large puzzles, you need to specify an option for larger JVM heap space.

scala -cp copris-nonogram-v1-2.jar -J-Xmx2g nonogram.Solver cwd_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. Specify the full path of the SAT solver program with "-s1" or "-s2" option.

scala -cp copris-nonogram-v1-2.jar nonogram.Solver -s1 glucose cwd_file_name

Example Usage

$ scala -cp copris-nonogram-v1-2.jar nonogram.Solver webpbn-00006.cwd
..##................
.##.................
.#..................
.#..................
.#.....###..........
##....#####.........
#....#######...#...#
#....########..##.##
#...#########..#####
##..################
.#.#################
.#######.###########
..#####...#####.###.
..#####...####......
...###.....###......
...##......##.......
..##........#.......
..#.........#.......
..##........##......
..##........##......
Unique solution

Performance Evaluation

Solver performance is measured on version 1.1.

Performance Comparison

The performance of many Nonogram solvers is reporeted in Survey of Paint-by-Number Puzzle Solvers by Jan Wolter. His web page is very well written with complehensive evalution and analysis of Nonogram solvers.

PuzzleSizeCoprisWuSyromolotovWolterOlsakSimpsonBGULager-kvistKjeller-strandKjeller-strand
/Gecode/Gecode/Lazyfd
#1: Dancer5 x 100.610.000.000.000.000.000.060.010.010.04
#6: Cat20 x 202.330.000.000.000.000.000.080.010.020.44
#21: Skid14 x 252.240.000.000.000.000.000.080.010.020.64
#27: Buck27 x 233.870.000.000.000.000.000.160.010.021.10
#23: Edge10 x 110.600.000.000.000.000.000.090.010.010.08
#2413: Smoke20 x 203.170.000.000.000.000.000.190.010.020.60
#16: Knot34 x 345.430.000.000.000.000.000.200.010.025.50
#529: Swing45 x 455.740.000.000.000.000.000.250.020.0413.20
#65: Mum34 x 405.430.000.010.010.000.010.260.020.0411.00
#7604: DiCap52 x 6310.370.010.110.020.000.002.100.020.06+
#1694: Tragic45 x 506.110.020.020.040.030.540.620.14216.0032.10
#1611: Merka55 x 608.420.020.010.010.010.000.350.03+66.00
#436: Petro40 x 355.050.010.040.0615.200.100.5884.001.606.20
#4645: M&M50 x 706.90-0.070.070.100.020.840.930.2848.10
#3541: Signed60 x 507.370.070.090.041.10324.000.680.570.5660.00
#803: Light50 x 454.710.200.190.38+0.021.10++4.70
#6574: Forever25 x 253.700.3413.903.702.0018.9044.304.702.301.70
#10810: Center60 x 6012.945.400.058.600.000.010.860.040.0727.80
#2040: Hot55 x 608.900.110.060.83+72.000.93++156.00
#6739: Karate40 x 406.440.060.030.8017.301098.000.6156.0057.8013.60
#8098: 9-Dom19 x 193.0120.3011.7011.00240.00+168.00756.003.801.80
#2556: Flag65 x 4539.07-0.020.551.500.0024.203.40+4.20
#2712: Lion47 x 4711.2953.4024.806.30++7.80+++
#10088: Marley52 x 6315.4954.004.20+++22.00++174.00
#18297: Thing36 x 4226.03504.00+402.00++120.00++216.00
#9892: Nature50 x 4038.58108.00++1116.00++++144.00
#12548: Sierp47 x 4049.19+132.00+++++++
  • The above table is constructed from the reported results in Jan Wolter's page updated on Wed Nov 21 19:38:58 PST 2012. The results of Copris solver is added to his results. Note that Copris is run on a faster machine.
  • The table shows the CPU time in seconds of each solver for each instance.
  • The CPU time includes the time for "uniqueness checking".
  • Copris solver was run on Intel Xeon 3.47GHz machine with:
    • Ubuntu Linux 12.04
    • Java version "1.6.0_27", OpenJDK Runtime Environment
    • Scala version 2.9.1
    • Copris version 2.0.0
    • Sugar version 2.0.0
    • Sat4j version 2.3.3
  • Other solvers were run on AMD Phenom II X4 810 2.6GHz machine.
  • "+" means the timeout (1800 seconds), and "-" means memory over.
  • nonogram-bach-sat4j233.log contains detailed results of Copris.

Note that Copris is the only solver which can solve all instances. The speed of Copris can be several times faster if you use other SAT solver such as Glucose, MiniSat, etc.

Results of Using Other SAT Solvers

The following table shows the results when other SAT solvers are used. The speed becomes faster than using Sat4j, but there are no big differences among other SAT solvers.

PuzzleSizeSat4jClaspGlucoseGlueMiniSatLingelingMiniSatPrecoSAT
#1: Dancer5 x 100.610.490.530.520.430.530.42
#6: Cat20 x 202.332.022.032.012.212.022.04
#21: Skid14 x 252.242.012.032.001.841.722.03
#27: Buck27 x 233.873.513.143.493.293.553.17
#23: Edge10 x 110.600.600.600.600.600.600.60
#2413: Smoke20 x 203.172.822.802.812.552.712.80
#16: Knot34 x 345.434.364.224.184.504.170.00
#529: Swing45 x 455.745.425.115.095.215.095.45
#65: Mum34 x 405.434.674.474.405.244.394.73
#7604: DiCap52 x 6310.378.447.036.738.087.027.16
#1694: Tragic45 x 506.115.435.235.195.505.095.20
#1611: Merka55 x 608.427.887.277.197.800.007.56
#436: Petro40 x 355.050.003.903.884.154.100.00
#4645: M&M50 x 706.906.655.956.097.165.546.20
#3541: Signed60 x 507.376.545.616.057.045.666.07
#803: Light50 x 454.714.694.153.905.374.044.47
#6574: Forever25 x 253.703.343.282.963.433.153.37
#10810: Center60 x 6012.9412.2312.2212.3013.3412.2112.54
#2040: Hot55 x 608.907.637.136.768.326.477.23
#6739: Karate40 x 406.445.365.215.295.875.245.41
#8098: 9-Dom19 x 193.012.302.202.072.832.072.32
#2556: Flag65 x 4539.074.284.964.344.335.444.25
#2712: Lion47 x 4711.297.887.287.098.246.935.97
#10088: Marley52 x 6315.4928.038.538.3215.868.359.69
#18297: Thing36 x 4226.039.279.328.7110.5911.278.73
#9892: Nature50 x 4038.589.8210.2912.2013.438.879.74
#12548: Sierp47 x 4049.1945.7016.7035.4021.2526.2521.33
Average10.857.465.606.286.615.655.50
  • The table shows the CPU time in seconds of Copris with each SAT solver for each instance.
  • Sat4j version 2.3.3
  • Clasp version 2.1.1
  • Glucose version 2.1 (without preprocessing)
  • GlueMiniSat version 2.2.5 (without preprocessing)
  • Lingeling version 587f
  • MiniSat version 2.2 (without preprocessing)
  • PrecoSAT version 576

Large Puzzles

Copris can solve very large puzzles.

PuzzleSizeSat4jClaspGlucoseGlueMiniSatLingelingMiniSatPrecoSAT
Artist75 x 1009.228.788.648.588.708.578.89
Balance100 x 758.728.288.018.208.378.018.49
Warship100 x 10010.7511.759.429.429.659.3610.05
#22336: Gettys99 x 59323.08111.7264.0655.3873.9089.7069.73
Average87.9435.1322.5320.4025.1628.9124.29

N-Dom Puzzles

The following table shows the performance of Copris to solve the n-Dom puzzles explained in Comparison of Solvers on the n-Dom Puzzles by Jan Wolter.

nSat4jClaspGlucoseGlueMiniSatLingelingMiniSatPrecoSAT
50.820.780.630.760.780.770.64
61.130.850.860.861.170.860.85
71.421.121.131.111.371.111.13
82.131.661.651.662.181.661.70
92.912.052.042.042.942.282.33
104.122.662.772.633.562.632.68
114.922.782.793.023.832.642.81
127.523.693.823.655.533.933.82
1311.734.374.914.617.634.874.77
1416.164.905.766.178.287.347.21
1521.589.909.458.7914.8916.868.26
1652.4818.6216.3913.4021.8517.0819.21
1775.9837.0020.3823.7535.5136.0237.39
18150.0967.4037.0033.2951.8988.0548.35
19278.08120.8253.6653.9593.0782.3593.74
20429.95170.0182.1778.03154.15195.80141.90
Average66.3128.0415.3414.8625.5429.0223.55
  • The table shows the CPU time in seconds of Copris with each SAT solver for each instance.
  • For clasp, "–configuration=jumpy" option is used.

Constraint Model

Input

  • \(m\) : number of rows
  • \(n\) : number of columns
  • \(rows(i)(k)\) : run length of the \(k\)-th block in the \(i\)-th row (\(i=0 .. m-1\))
  • \(cols(j)(k)\) : run length of the \(k\)-th block in the \(j\)-th column (\(j=0 .. n-1\))

CSP Variables

  • \(x(i,j) \in \{0, 1\}\): color of \((i,j)\) cell (0: white, 1: black)
  • \(r(i,k) \in \{0 .. n-rows(i)(k)\}\): left-most position of the \(k\)-th block in the \(i\)-th row
  • \(c(j,k) \in \{0 .. m-cols(j)(k)\}\): top-most position of the \(k\)-th block in the \(j\)-th column

Constraints

  • Blocks are not overlapped each other.
    • \(r(i,k) + rows(i)(k) < r(i,k+1)\)
    • \(c(j,k) + cols(j)(k) < c(j,k+1)\)
  • The \((i,j)\) cell is black iff it is contained in some block.
    • \(x(i,j)=1 \Leftrightarrow \bigvee_k (r(i,k) \le j \;\land\; j < r(i,k)+rows(i,k))\)
    • \(x(i,j)=1 \Leftrightarrow \bigvee_k (c(j,k) \le i \;\land\; i < c(j,k)+cols(j,k))\)

Source Code

The following shows the source code of the solver (Nonogram-v1-2.scala).

 1:  /*
 2:   * Nonogram Solver in Copris
 3:   * by Naoyuki Tamura
 4:   * http://bach.istc.kobe-u.ac.jp/copris/puzzles/nonogram/
 5:   */
 6:  package nonogram
 7:  import jp.kobe_u.copris._
 8:  import jp.kobe_u.copris.dsl._
 9:  import scala.io.Source
10:  
11:  object Solver {
12:    var m = 0
13:    var n = 0
14:    var rows: Seq[Seq[Int]] = Seq.empty
15:    var cols: Seq[Seq[Int]] = Seq.empty
16:    def parse(source: Source) = {
17:      val lines = source.getLines.map(_.trim)
18:      m = lines.next.toInt
19:      n = lines.next.toInt
20:      rows = for (i <- 0 until m; s = lines.next)
21:             yield if (s == "") Seq.empty
22:                   else s.split("\\s+").toSeq.map(_.toInt)
23:      lines.next
24:      cols = for (j <- 0 until n; s = lines.next)
25:             yield if (s == "") Seq.empty
26:                   else s.split("\\s+").toSeq.map(_.toInt)
27:      source.close
28:    }
29:    def define = {
30:      for (i <- 0 until m; j <- 0 until n)
31:        int('x(i,j), 0, 1)
32:      for (i <- 0 until m; k <- 0 until rows(i).size)
33:        int('r(i,k), 0, n-rows(i)(k))
34:      for (i <- 0 until m; k <- 0 until rows(i).size-1)
35:        add('r(i,k) + rows(i)(k) < 'r(i,k+1))
36:      for (j <- 0 until n; k <- 0 until cols(j).size)
37:        int('c(j,k), 0, m-cols(j)(k))
38:      for (j <- 0 until n; k <- 0 until cols(j).size-1)
39:        add('c(j,k) + cols(j)(k) < 'c(j,k+1))
40:      for (i <- 0 until m; j <- 0 until n) {
41:        val rs = for (k <- 0 until rows(i).size)
42:                 yield 'r(i,k) <= j && 'r(i,k) + rows(i)(k) > j
43:        add('x(i,j) > 0 <==> Or(rs))
44:        val cs = for (k <- 0 until cols(j).size)
45:                 yield 'c(j,k) <= i && 'c(j,k) + cols(j)(k) > i
46:        add('x(i,j) > 0 <==> Or(cs))
47:      }
48:    }
49:    def showSolution = {
50:      for (i <- 0 until m) {
51:        val xs = for (j <- 0 until n)
52:                 yield if (solution('x(i,j)) == 0) "." else "#"
53:        println(xs.mkString)
54:      }
55:    }
56:    def main(args: Array[String]) = {
57:      val name = "nonogram.Solver"
58:      var help = false
59:      var quiet = false
60:      def parseOptions(args: List[String]): List[String] = args match {
61:        case "-h" :: rest =>
62:          { help = true; parseOptions(rest) }
63:        case "-s1" :: solver :: rest =>
64:          { use(new sugar.Solver(csp, new sugar.SatSolver1(solver))); parseOptions(rest) }
65:        case "-s2" :: solver :: rest =>
66:          { use(new sugar.Solver(csp, new sugar.SatSolver2(solver))); parseOptions(rest) }
67:        case "-smt" :: solver :: rest =>
68:          { use(new smt.Solver(csp, new smt.SmtSolver(solver))); parseOptions(rest) }
69:        case "-q" :: rest =>
70:          { quiet = true; parseOptions(rest) }
71:        case _ =>
72:          args
73:      }
74:      parseOptions(args.toList) match {
75:        case Nil if ! help =>
76:          parse(Source.stdin)
77:        case file :: Nil if ! help =>
78:          parse(Source.fromFile(file))
79:        case _ => {
80:          println("Usage: scala " + name + " [options] [inputFile]")
81:          println("\t-h          : Help")
82:          println("\t-q          : Quiet output")
83:          println("\t-s1 solver  : Use SAT solver (minisat, etc.)")
84:          println("\t-s2 solver  : Use SAT solver (precosat, etc.)")
85:          println("\t-smt solver : Use SMT solver (z3, etc.)")
86:          System.exit(1)
87:        }
88:      }
89:      define
90:      if (find) {
91:        if (! quiet)
92:          showSolution
93:        if (findNext)
94:          println("Multiple solutions")
95:        else
96:          println("Unique solution")
97:      }
98:    }
99:  }

License

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

Links

?????

Date: 2014-07-05 23:29:02 JST

Author: Naoyuki Tamura

Org version 7.8.02 with Emacs version 24

Validate XHTML 1.0