Sudoku Solver in Copris

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

This Sudoku solver can find a solution of the given Sudoku puzzle.

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)

• 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 sudoku.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-puzzles-2.0.jar sudoku.Solver -o multi input_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 sudoku.Solver -o multi -s2 minisat input_file_name

Solver performance is measured on version 2.0.

• Copris solver was run on Intel Xeon 3.6Hz machine with:
  • Ubuntu Linux 20.04 (64 bit)
  • Java version "1.8.0_275", OpenJDK Runtime Environment (with "-Xmx2G" option)
  • Scala version 2.12.5
  • Copris version 2.3.1
  • Sugar version 2.3.4
• GlueMiniSat version 2.2.10 (with preprocessing) is used as a SAT solver.

The following shows the source code of the solver (Sudoku.scala).

 1:  /*
 2:   * Sudoku Solver in Copris
 3:   * by Naoyuki Tamura
 4:   * http://bach.istc.kobe-u.ac.jp/copris/puzzles/sudoku/
 5:   */
 6:  package sudoku
 7:  
 8:  import jp.kobe_u.copris._
 9:  import jp.kobe_u.copris.dsl._
10:  import puzzle._
11:  
12:  case class Sudoku(m: Int, n: Int, dm: Int, dn: Int, board: Seq[Seq[String]]) extends BoardPuzzle {
13:    require(m == n && m == dm * dn)
14:    def show(sol: Seq[Seq[Int]]) {
15:      for (i <- 0 until m) {
16:        for (j <- 0 until n)
17:          print("%3d".format(sol(i)(j)))
18:        println
19:      }
20:    }
21:  }
22:  
23:  object Solver extends BoardPuzzleSolver[Sudoku] {
24:    val name = "sudoku.Solver"
25:  
26:    def puzzleFactory(m: Int, n: Int, dm: Int, dn: Int, board: Seq[Seq[String]]) =
27:      Sudoku(m, n, dm, dn, board)
28:  
29:    override def puzzleFactory(m: Int, n: Int, board: Seq[Seq[String]]) = {
30:      val dm = math.sqrt(m).toInt
31:      require(m == n && m == dm * dm)
32:      puzzleFactory(m, n, dm, dm, board)
33:    }
34:  
35:    override def parse(source: scala.io.Source) = {
36:      val lines = source.getLines.map(_.trim).filter(! _.startsWith(";"))
37:      val ms = lines.next.split("\\s+").map(_.toInt)
38:      val m = ms(0)
39:      val dm = if (ms.size >= 2) ms(1) else math.sqrt(m).toInt
40:      val ns = lines.next.split("\\s+").map(_.toInt)
41:      val n = ns(0)
42:      val dn = if (ns.size >= 2) ns(1) else math.sqrt(n).toInt
43:      val board = for (i <- 0 until m; s = lines.next)
44:                  yield s.split("\\s+").toSeq
45:      source.close
46:      puzzleFactory(m, n, dm, dn, board)
47:    }
48:  
49:    def alldiff(xs: Seq[Term]) {
50:      add(Alldifferent(xs))
51:      for (a <- 1 to puzzle.m)
52:        add(Or(xs.map(x => x === a)))
53:    }
54:  
55:    def define {
56:      for (cell <- puzzle.cells)
57:        if (puzzle.isNumber(cell))
58:          int('x(cell), puzzle.num(cell))
59:        else
60:          int('x(cell), 1, puzzle.m)
61:      for (i <- 0 until puzzle.m)
62:        alldiff((0 until puzzle.n).map(j => 'x((i,j))))
63:      for (j <- 0 until puzzle.n)
64:        alldiff((0 until puzzle.m).map(i => 'x((i,j))))
65:      for (i <- 0 until puzzle.m by puzzle.dm; j <- 0 until puzzle.n by puzzle.dn) {
66:        val xs = for (di <- 0 until puzzle.dm; dj <- 0 until puzzle.dn)
67:                 yield 'x((i+di,j+dj))
68:        alldiff(xs)
69:      }
70:    }
71:  
72:    def showSolution {
73:      val sol = for (i <- 0 until puzzle.m)
74:                yield (0 until puzzle.n).map(j => solution('x((i,j))))
75:      if (quiet == 0) {
76:        println("Solution = " + sol)
77:        println("Size = " + sol.size)
78:        puzzle.show(sol)
79:      }
80:    }
81:  }

• It should be compiled with ../build/PuzzleSolver.scala.

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
• Sudoku (by Nikoli)
• Wikipedia:Sudoku
• http://www.janko.at/Raetsel/Sudoku/