Scribd
Upload
320 views4 pages

World's Hardest Sudoku

This document discusses solving the "world's hardest Sudoku" puzzle using a SAT solver in Maple. It describes representing the Sudoku puzzle as a Boolean satisfiability problem by defining variables for each cell and digit combination, and generating positive and negative constraints representing the Sudoku rules. The SAT solver is then used to find an assignment satisfying all the constraints, solving the puzzle. Finally, functions are provided to visualize the solved puzzle on a Sudoku grid.

Uploaded by

Việt Hải Trần
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
320 views4 pages

World's Hardest Sudoku

This document discusses solving the "world's hardest Sudoku" puzzle using a SAT solver in Maple. It describes representing the Sudoku puzzle as a Boolean satisfiability problem by defining variables for each cell and digit combination, and generating positive and negative constraints representing the Sudoku rules. The SAT solver is then used to find an assignment satisfying all the constraints, solving the puzzle. Finally, functions are provided to visualize the solved puzzle on a Sudoku grid.

Uploaded by

Việt Hải Trần
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
You are on page 1/ 4

Solving the World's Hardest

Sudoku

Sudoku is a popular puzzle that appears in many puzzle books and


newspapers.
Given a 9 by 9 grid whose squares are either blank or contain a number
between 1 and 9, the objective is to fill in the blank squares in such a way so
that each row and column contains exactly one digit between 1 and 9.
Additionally, each of the nine 3 by 3 subgrids which compose the grid
(called blocks) must also contain exactly one digit between 1 and 9.
The mathematician Arto Inkala published the "world's hardest Sudoku"
(shown above). The puzzle has been estimated to have a difficulty rating of
11 stars, whereas the most challenging Sudoku puzzles that are usually
published are given a difficulty of 5 stars.
Using Maple's built-in efficient SAT solver we can quickly solve this puzzle
without any knowledge of Sudoku solving techniques. A SAT solver takes
as input a formula in Boolean logic and returns an assignment to the
variables that makes the formula true (if one exists). See the Satisfy
command for more information.

Setting up the problem


We'll use the Boolean variables for to denote that
the square contains the digit .
We'll also use a few simple functions to compute the set of variables
which appear in the same row, column, or block as the square and
concern the digit :

Generating the constraints


To encode the rules of Sudoku in Boolean logic we want to encode both
positive and negative constraints.
Positive constraints say that each square must contain some digit.
Negative constraints say that each square cannot contain more than one
digit and that squares in the same row, column, or block do not contain
the same digit twice.
Positive constraints
For each square at least one digit appears in the square.
These clauses have the form for
each .

Negative constraints
For each square if the digit appears in that square then no other
digit appears in that square.
These clauses have the form (alternatively,
) where is a digit with .

For each square if the digit appears in that square then the digit
does not appear in any other square in the same row, column, or
block.
These clauses have the form where is in the set
.

Finding a solution
We also need to specify the 21 numbers which are given to us as a part of
the puzzle; if contains then we need to include the unit clause
in our SAT instance. The clauses resulting from the world's
hardest Sudoku are as follows:

We use the Satisfy command from the Logic package which finds a
satisfying assignment of a logical formula if one exists.
We use the Usage command from the CodeTools package to measure
how quickly the solution is found.
Visualization of the solution
The following functions use commands from the plots and plottools
packages to draw a Sudoku grid and fill in numbers on the grid.

The following code draws the Sudoku grid with the digits from the
solution found by the SAT solver.

You might also like