How Mace4 does Sudoku

Mace4 Background

Mace4 is a finite domain constraint solver. The constraints are given as statements in first-order logic with equality.

Mace4 is used primarily for two purposes:

Sudoku Specifications for Mace4

It turns out that Sudoku puzzles are straightforward to specify in the language of Mace4.

Here is a Mace4 job that solves a particular Sudoku puzzle.

    mace4 -m -1 -f > example.out
See the input and output files (the solution is in "function(f(_,_) ...").

Our Web interface simply constructs an input file similar to and runs Mace4 on it.

Colors in the answers.

Ok, let's do Sudoku!

Back to Home