Package org.sosy_lab.java_smt.example

Class Sudoku

java.lang.Object

org.sosy_lab.java_smt.example.Sudoku

public class Sudoku
extends Object

This program parses user-given Sudoku and solves it with an SMT solver.

This program is just an example and provides several distinct strategies for encoding the Sudoku problem as SMT. Clearly SMT is not the best solution for solving Sudoku. There might be other algorithms out there that are specialized and better suited for solving Sudoku.

Our strategies:

• Integer-based: We encode all values as integer formulas for a range from 1 to 9. Straight forward, simple to understand, but slow.
• Enumeration-based: We encode all values as enumeration formulas for enumeration values from ONE to NINE. Reasonable fast (up to 10x faster than integer-based strategy).
• Boolean-based: We use one more dimension to encode values for the 2D-grid and a one-hot-encoding. Fastest SMT-based solution, because it is purely based on SAT, and no additional SMT theory is applied.

The more numbers are available in a Sudoku, the easier it can be solved. A completely empty Sudoku will cause the longest runtime in the solver, because it will guess a lot of values.

The Sudoku is read from StdIn and should be formatted as the following example:

 2..9.6..1
 ..6.4...9
 ...52.4..
 3.2..7.5.
 ...2..1..
 .9.3..7..
 .87.5.31.
 6.3.1.8..
 4....9...
 

The solution will then be printed on StdOut, just like the following solution:

 248976531
 536148279
 179523468
 312487956
 764295183
 895361742
 987652314
 623714895
 451839627
 

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	Sudoku.BooleanBasedSudokuSolver
static class	Sudoku.EnumerationBasedSudokuSolver
static class	Sudoku.IntegerBasedSudokuSolver
static class	Sudoku.SudokuSolver<S>

Field Summary

Fields

Modifier and Type	Field	Description
static int	SIZE

Method Summary

Modifier and Type	Method	Description
static void	main(String... args)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

SIZE

public static final int SIZE

See Also:

Constant Field Values

Method Detail

main

public static void main(String... args)
                 throws InvalidConfigurationException,
                        SolverException,
                        InterruptedException,
                        IOException

Throws:

InvalidConfigurationException

SolverException

InterruptedException

IOException