Nonogram Solver in Copris

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.

Version 2.0

• Scala jar file: ../build/copris-puzzles-2.0.jar (1575981 bytes)
• Source file: ../build/copris-puzzles-src-2.0.zip (29766 bytes)

Multicolor version

• Please visit Multicolor Nonogram Solver in Copris page by Jan Wolter.

• 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)

scala -cp copris-puzzles-2.0.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-puzzles-2.0.jar -J-Xmx2g nonogram.Solver cwd_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 nonogram.Solver -s2 minisat cwd_file_name

Solver performance is measured on version 1.1 in 2013.

The following shows the source code of the solver (Nonogram.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 "-jsr331" :: rest =>
 70:          { use(new jsr331.Solver(csp)); parseOptions(rest) }
 71:        case "-pb" :: solver :: encoding :: rest =>
 72:          { use(new pb.Solver(csp, new pb.PbSolver(solver), encoding)); parseOptions(rest) }
 73:        case "-q" :: rest =>
 74:          { quiet = true; parseOptions(rest) }
 75:        case _ =>
 76:          args
 77:      }
 78:      parseOptions(args.toList) match {
 79:        case Nil if ! help =>
 80:          parse(Source.stdin)
 81:        case file :: Nil if ! help =>
 82:          parse(Source.fromFile(file))
 83:        case _ => {
 84:          println("Usage: scala " + name + " [options] [inputFile]")
 85:          println("\t-h          : Help")
 86:          println("\t-q          : Quiet output")
 87:          println("\t-s1 solver  : Use SAT solver (minisat, etc.)")
 88:          println("\t-s2 solver  : Use SAT solver (precosat, etc.)")
 89:          println("\t-smt solver : Use SMT solver (z3, etc.)")
 90:          println("\t-jsr331     : Use JSR331 solver")
 91:          println("\t-pb solver encoding : Use PB solver (clasp, etc.)")
 92:          System.exit(1)
 93:        }
 94:      }
 95:      define
 96:      if (find) {
 97:        if (! quiet)
 98:          showSolution
 99:        if (findNext)
100:          println("Multiple solutions")
101:        else
102:          println("Unique solution")
103:      }
104:    }
105:  }

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

• Copris (Constraint Programming DSL embedded in Scala)
• Sugar (an award winning Constraint Solver)
  • Default constraint solver used in Copris
• Sat4j (SAT solver in Java)
  • Default SAT solver used in Copris
• Wikipedia: Nonogram
• Survey of Paint-by-Number Puzzle Solvers (by Jan Wolter)
  • Multicolor Nonogram Solver in Copris
• Nonogram Solver (by Steven Simpson)
• Update on Nonogram (by Hakan Kjellerstrand)
• http://www.janko.at/Raetsel/Nonogramme/