Package org.sosy_lab.java_smt.example

Class Binoxxo

java.lang.Object

org.sosy_lab.java_smt.example.Binoxxo

public final class Binoxxo
extends Object

This program parses a user-given Binoxxo and solves it with an SMT solver. Binoxxo is a grid-based Sudoku-like puzzle with values 'O' and 'X' and follows the following rules:

• In each column or row there are as many 'X's as 'O's.
• Three aligned cells must not contains an identical value.

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

 X..O...XX.
 .O.O....X.
 OO..O..X..
 ...O....X.
 .O........
 .O.....O.X
 X...X.O...
 .X..XO...X
 X.....OO..
 X..X..O..O
 

A empty newline will terminate the input and start the solving process.

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

 XXOOXOOXXO
 OOXOOXXOXX
 OOXXOOXXOX
 XXOOXXOOXO
 OOXXOOXXOX
 OOXXOXXOOX
 XXOOXXOOXO
 OXOOXOXXOX
 XOXXOXOOXO
 XXOXXOOXOO
 

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	Binoxxo.BinoxxoSolver<S>
static class	Binoxxo.BooleanBasedBinoxxoSolver	This solver encodes nore steps into boolean logic, which makes it about 10x faster than the Binoxxo.IntegerBasedBinoxxoSolver.
static class	Binoxxo.IntegerBasedBinoxxoSolver

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

Method Detail

main

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

Throws:

InvalidConfigurationException

SolverException

InterruptedException

IOException