# 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:

- 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.

## 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.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.

- White: given,
- Green: determined without guessing (there might be more),
- Red: found after start of case analysis.

Ok, let's do Sudoku!

Back to Home