How Mace4 does Sudoku

October, 2005.

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:

in conjuction with an automated theorem-proving program such as Otter or Prover9, to look for finite counterexamples, and
for research in abstract algebra and logic.

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.in > example.out

See the input and output files (the solution is in "function(f(_,_) ...").

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

Colors in the answers.