/*
 * Nonogram Solver in Copris
 * by Naoyuki Tamura
 * http://bach.istc.kobe-u.ac.jp/copris/puzzles/nonogram/
 * Modified to solve multicolor nonograms by Jan Wolter
 */
package nonogram
import jp.kobe_u.copris._
import jp.kobe_u.copris.sugar.dsl._
import scala.io.Source

object Solver {
  var m = 0
  var n = 0
  var nc = 0
  var rown: Seq[Seq[Int]] = Seq.empty
  var coln: Seq[Seq[Int]] = Seq.empty
  var rowc: Seq[Seq[Int]] = Seq.empty
  var colc: Seq[Seq[Int]] = Seq.empty
  def parse(source: Source) = {
    val lines = source.getLines.map(_.trim)
    m = lines.next.toInt
    n = lines.next.toInt
    nc = lines.next.toInt
    rown = for (i <- 0 until m; val s = lines.next)
	   yield if (s == "") Seq.empty
		 else s.split("\\s+").toSeq.map(_.toInt)
    lines.next
    rowc = for (i <- 0 until m; val s = lines.next)
	   yield if (s == "") Seq.empty
		 else s.split("\\s+").toSeq.map(_.toInt)
    lines.next
    coln = for (j <- 0 until n; val s = lines.next)
	   yield if (s == "") Seq.empty
		 else s.split("\\s+").toSeq.map(_.toInt)
    lines.next
    colc = for (j <- 0 until n; val s = lines.next)
	   yield if (s == "") Seq.empty
		 else s.split("\\s+").toSeq.map(_.toInt)
    source.close
  }
  def define = {
    for (i <- 0 until m; j <- 0 until n)
      int('x(i,j), 0, nc)

    for (i <- 0 until m; k <- 0 until rown(i).size)
      int('r(i,k), 0, n-rown(i)(k))
    for (i <- 0 until m; k <- 0 until rown(i).size-1
         if rowc(i)(k) == rowc(i)(k+1))
      add('r(i,k) + rown(i)(k) < 'r(i,k+1))
    for (i <- 0 until m; k <- 0 until rown(i).size-1
	 if rowc(i)(k) != rowc(i)(k+1))
      add('r(i,k) + rown(i)(k) <= 'r(i,k+1))

    for (j <- 0 until n; k <- 0 until coln(j).size)
      int('c(j,k), 0, m-coln(j)(k))
    for (j <- 0 until n; k <- 0 until coln(j).size-1
	 if colc(j)(k) == colc(j)(k+1))
      add('c(j,k) + coln(j)(k) < 'c(j,k+1))
    for (j <- 0 until n; k <- 0 until coln(j).size-1
	 if colc(j)(k) != colc(j)(k+1))
      add('c(j,k) + coln(j)(k) <= 'c(j,k+1))

    for (i <- 0 until m; j <- 0 until n; v <- 1 until nc+1) {
      val rs = for (k <- 0 until rown(i).size if rowc(i)(k) == v)
	       yield 'r(i,k) <= j && 'r(i,k) + rown(i)(k) > j
      add(('x(i,j) === v) <==> Or(rs))
      val cs = for (k <- 0 until coln(j).size if colc(j)(k) == v)
	       yield 'c(j,k) <= i && 'c(j,k) + coln(j)(k) > i
      add(('x(i,j) === v) <==> Or(cs))
    }
  }
  def showSolution = {
    for (i <- 0 until m) {
      val xs = for (j <- 0 until n)
	       yield if (solution('x(i,j)) == 0) "." else solution('x(i,j))
      println(xs.mkString)
    }
  }
  def main(args: Array[String]) = {
    val name = "nonogram.Solver"
    var help = false
    var quiet = false
    def parseOptions(args: List[String]): List[String] = args match {
      case "-h" :: rest =>
	{ help = true; parseOptions(rest) }
      case "-s1" :: solver :: rest =>
	{ use(new sugar.SatSolver1(solver)); parseOptions(rest) }
      case "-s2" :: solver :: rest =>
	{ use(new sugar.SatSolver2(solver)); parseOptions(rest) }
      case "-q" :: rest =>
	{ quiet = true; parseOptions(rest) }
      case _ =>
	args
    }
    parseOptions(args.toList) match {
      case Nil if ! help =>
	parse(Source.stdin)
      case file :: Nil if ! help =>
	parse(Source.fromFile(file))
      case _ => {
        println("Usage: scala " + name + " [options] [inputFile]")
	println("\t-h         : Help")
	println("\t-q         : Quiet output")
	println("\t-s1 solver : Use SAT solver (minisat, etc.)")
	println("\t-s2 solver : Use SAT solver (precosat, etc.)")
	System.exit(1)
      }
    }
    define
    if (find) {
      if (! quiet)
	showSolution
      if (findNext)
	println("Multiple solutions")
      else
	println("Unique solution")
    }
  }
}