Proven Sudoku
Techniques / Brute force and theory
SAT and Constraint Programming Encodings
Also called SAT encoding, CP encoding, Boolean encoding.
New to this shorthand? How to read a sudoku grid explains r4c7, houses, candidates and the rest.
What it means
The puzzle is turned into a long list of yes or no questions. Then a general solver works through them. It is a job for a computer, not for a person.
The exact rule, for stronger players
The rule, stated exactly: Encode the grid as boolean variables, one per cell-digit pair, with clauses enforcing at least one and at most one digit per cell and per house, then apply a general SAT or constraint solver.
What it removes: Not an elimination technique.
Why it works: The encoding is a faithful translation, so any model of the formula is a valid grid.
Worked examples
None yet. This pattern does not turn up in our daily boards, so there is no real example to show. We would rather wait than draw a fake one.
Learn these first
- Exact Cover and Dancing LinksA sudoku can be rewritten as a tidy tick box puzzle.
Related brute force
- Unavoidable Sets and Puzzle GenerationAn unavoidable set is a group of squares you could rearrange to get a second answer.
- Difficulty Rating EnginesPrograms give a puzzle a score.
- Minimal Puzzles and the 17-Clue ResultA puzzle is minimal when you cannot take away any clue without giving it a second answer.
How often does it come up?
Our rough estimate: not a solving technique. Included because it explains why brute force is fast and why puzzle difficulty for humans has nothing to do with difficulty for machines.