Sudoku Solver in Copris

Table of Contents

Overview

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.

What's New

  • 2013-10-14 Mon Release of version 1.1
  • 2013-09-01 Sun First release

Download

Version 1.1
Version 1.0

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-sudoku-v1-1.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-sudoku-v1-1.jar sudoku.Solver -o multi input_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.

scala -cp copris-sudoku-v1-1.jar sudoku.Solver -o multi -s1 glucose input_file_name

Input file format

The following is an example of input file.

9
9
2 1 - 4 - - - 3 6
8 - - - - - - - 5
- - 5 3 - 9 8 - -
6 - 4 9 - 7 1 - -
- - - - 3 - - - -
- - 7 5 - 4 6 - 2
- - 6 2 - 3 5 - -
5 - - - - - - - 9
9 3 - - - 5 - 2 7
  • The first line gives the number of rows, and the row size of each block (optional).
  • The second line gives the number of columns, and the column size of each block (optional).
  • Number cells are represented by its number.
  • Blank cells are represented by "-".

Example Usage

$ scala -cp copris-sudoku-v1-0.jar sudoku.Solver data/001.a.txt 
BEGIN_solution = 1
Solution = Vector(Vector(2, 1, 9, 4, 5, 8, 7, 3, 6), Vector(8, 4, 3, 1, 7, 6, 2, 9, 5), Vector(7, 6, 5, 3, 2, 9, 8, 4, 1), Vector(6, 2, 4, 9, 8, 7, 1, 5, 3), Vector(1, 5, 8, 6, 3, 2, 9, 7, 4), Vector(3, 9, 7, 5, 1, 4, 6, 8, 2), Vector(4, 7, 6, 2, 9, 3, 5, 1, 8), Vector(5, 8, 2, 7, 4, 1, 3, 6, 9), Vector(9, 3, 1, 8, 6, 5, 4, 2, 7))
Size = 9
  2  1  9  4  5  8  7  3  6
  8  4  3  1  7  6  2  9  5
  7  6  5  3  2  9  8  4  1
  6  2  4  9  8  7  1  5  3
  1  5  8  6  3  2  9  7  4
  3  9  7  5  1  4  6  8  2
  4  7  6  2  9  3  5  1  8
  5  8  2  7  4  1  3  6  9
  9  3  1  8  6  5  4  2  7
END_solution = 1
NumOfSolutions >= 1

Performance Evaluation

Solver performance is measured on version 1.0.

  • Copris solver was run on Intel Xeon 3.47GHz machine with:
    • Ubuntu Linux 12.04 (32 bit)
    • Java version "1.6.0_27", OpenJDK Runtime Environment (with "-Xmx2G" option)
    • Scala version 2.9.1
    • Copris version 2.0.0
    • Sugar version 2.0.0
  • Glucose version 2.1 (with preprocessing) is used as a SAT solver.

Finding a solution

Source Code

The following shows the source code of the solver (Sudoku-v1-1.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 define = {
50:      for (cell <- puzzle.cells)
51:        if (puzzle.isNumber(cell))
52:          int('x(cell), puzzle.num(cell))
53:        else
54:          int('x(cell), 1, puzzle.m)
55:      for (i <- 0 until puzzle.m)
56:        add(Alldifferent((0 until puzzle.n).map(j => 'x((i,j)))))
57:      for (j <- 0 until puzzle.n)
58:        add(Alldifferent((0 until puzzle.m).map(i => 'x((i,j)))))
59:      for (i <- 0 until puzzle.m by puzzle.dm; j <- 0 until puzzle.n by puzzle.dn) {
60:        val xs = for (di <- 0 until puzzle.dm; dj <- 0 until puzzle.dn)
61:                 yield 'x((i+di,j+dj))
62:        add(Alldifferent(xs))
63:      }
64:    }
65:  
66:    def showSolution {
67:      val sol = for (i <- 0 until puzzle.m)
68:                yield (0 until puzzle.n).map(j => solution('x((i,j))))
69:      if (quiet == 0) {
70:        println("Solution = " + sol)
71:        println("Size = " + sol.size)
72:        puzzle.show(sol)
73:      }
74:    }
75:  }

License

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

Links

?????

Date: 2013-12-01 10:41:55 JST

Author: Naoyuki Tamura

Org version 7.8.02 with Emacs version 23

Validate XHTML 1.0