数独をSATソルバを用いて解く

sat_sudoku.sh

#!/bin/bash -e

type sat13 > /dev/null

if [[ $# -eq 2  && $1 = "-x" ]]; then
    scala -nc SudokuEncode $2
    sat13 < tmp.sat | tr ' ' '\n' | grep -v '^~' | sort -n | sed "/^$/d" > ans.sat
    scala -nc SudokuShow
    rm tmp.sat ans.sat
else
    case $1 in
        "-c" )
            echo "Complile scala scripts..."
            scalac sudoku_encode.scala sudoku_show.scala ;;
        "-d" )
            echo "Delete scala class files..."
            rm *.class ;;
        * )
            scala -nc sudoku_encode.scala $1
            sat13 < tmp.sat | tr ' ' '\n' | grep -v '^~' | sort -n | sed "/^$/d" > ans.sat
            scala -nc sudoku_show.scala
            rm tmp.sat ans.sat
    esac
fi

sudoku_encode.scala

import scala.io.Source
import java.io._

/*case class Cell(i: Int, j: Int, n: Int, not: Boolean = false) {
  override def toString: String = (if (not) "~" else "") + s"${i},${j},${n}"
  def unary_! = Cell(i, j, n, !not)
}*/

abstract class Sudoku {
  protected def url: String

  def getTable: Seq[Seq[Int]] = {
    println("Sudoku from " + url)
    val src = Source.fromURL(url)
    val lines = src.getLines().toSeq
    src.close
    extractTable(lines)
  }

  protected def extractTable(lines: Seq[String]): Seq[Seq[Int]]
}

final class JankoSudoku(val number: Int) extends Sudoku {
  override protected def url: String = "https://www.janko.at/Raetsel/Sudoku/" + "%04d".format(number) + ".a.htm"

  override protected def extractTable(lines: Seq[String]): Seq[Seq[Int]] = {
    val top = lines.indexOf("problem")
    for (i <- 1 to 9) yield {
      lines(top+i).split("\\s+").map {
        case "-" | "." => 0
        case a => a.toInt
      }.toSeq
    }
  }
}

object JankoSudoku {
  def apply(number: Int): JankoSudoku = new JankoSudoku(number)
}


object SudokuEncode {
  def cell(i: Int, j: Int, n: Int, not: Boolean = false): String =
    (if (not) "~" else "") + s"${i},${j},${n}"

  def main(args: Array[String]): Unit = {
    // 0 <= All value <= 9
    /*val valueRanges = for (i <- 1 to 9; j <- 1 to 9) yield {
        for (n <- 1 to 9) yield cell(i, j, n)
    }*/
    val valueRanges = for (i <- 1 to 9; j <- 1 to 9) yield (1 to 9).map(cell(i, j, _))

    // Different numbers in rows and columns
    val consRowCol = (for (r <- 1 to 9; i <- 1 until 9; j <- i+1 to 9; n <- 1 to 9)
      yield Seq(
        Seq(cell(r, i, n, not = true), cell(r, j, n, not = true)),
        Seq(cell(i, r, n, not = true), cell(j, r, n, not = true))
      )).flatten

    /*
    // Different numbers in rows
    val consRow = for (r <- 1 to 9; i <- 1 to 9; j <- i+1 to 9; n <- 1 to 9)
      yield Seq(cell(r, i, n, not = true), cell(r, j, n, not = true))

    // Different numbers in columns
    val consCol = for (c <- 1 to 9; i <- 1 to 9; j <- i+1 to 9; n <- 1 to 9)
      yield Seq(cell(i, c, n, not = true), cell(j, c, n, not = true))
    */

    // Different numbers in block
    /*
    val cordPairs = Seq(1, 2, 3, 1, 2, 3).combinations(2).flatMap(_.permutations).toSeq.combinations(2)
    val consBlock = for {
      l <- 0 until 9 by 3
      m <- 0 until 9 by 3
      pair <- cordPairs
      n <- 1 to 9
    } yield Seq(
      !Cell(l+pair(0)(0), m+pair(0)(1), n),
      !Cell(l+pair(1)(0), m+pair(1)(1), n))
    */
    val consBlock = for {
      l <- 0 until 9 by 3
      m <- 0 until 9 by 3
      i1 <- 1 to 2
      j1 <- 1 to 3
      i2 <- j1 to 3
      j2 <- (1 to 3).filter(_ != j1)
      n <- 1 to 9
    } yield Seq(cell(l+i1, m+j1, n, not = true), cell(l+i2, m+j2, n, not = true))

    // only one in row and column
    val consOnlyRowCol = (for (i <- 1 to 9; n <- 1 to 9)
      yield Seq(
        (1 to 9).map(cell(i, _, n)),
        (1 to 9).map(cell(_, i, n))
      )).flatten

    // only one in block
    val cords = Seq(1, 2, 3, 1, 2, 3).combinations(2).flatMap(_.permutations).toSeq
    val consOnlyBlock = for {
      l <- 0 until 9 by 3
      m <- 0 until 9 by 3
      n <- 1 to 9
    } yield cords.map(p => cell(l+p(0), m+p(1), n))


    // Get sudoku table
    val sudoku = JankoSudoku(args(0).toInt)
    val t = sudoku.getTable
    val constSet = t.map(a => a.zipWithIndex.filter(b => b._1 != 0))
    val consCell = constSet.zipWithIndex.flatMap(
      a => a._1.map(b => cell(a._2+1, b._2+1, b._1))
    )

    val clauses =
      valueRanges ++ consRowCol ++ consBlock ++ consOnlyRowCol ++ consOnlyBlock ++ consCell
    //val clauses = valueRanges ++: consRow ++: consCol ++: consBlock ++: consCell

    val writer = new BufferedWriter((new FileWriter("tmp.sat")))
    clauses.map {
      case c: Seq[_] => c.mkString(" ") + '\n'
      case s: String => s + '\n'
      //case d: Cell => d.toString + '\n'
    }.foreach(writer.write)
    writer.close()
  }
}

sudoku_show.scala

import scala.io.Source

object SudokuShow {
  def main(args: Array[String]): Unit = {
    val s = Source.fromFile("ans.sat")
    val lines = s.getLines.toSeq
    s.close

    val nums = lines.map(_.split(",").last)

    println("+---+---+---+---+---+---+---+---+---+")
    for (i <- 0 until 9) {
      println("| " + nums.slice(9*i, 9*(i+1)).mkString(" | ") + " |")
      println("+---+---+---+---+---+---+---+---+---+")
    }
  }
}