Page 53 - Discrete Mathematics and Its Applications

32 1 / The Foundations: Logic and Proofs

29 4
5 1
4
42
6 7
5
7 3 5
1 9
6

FIGURE 1 A9 × 9 Sudoku puzzle.

Applications of Satisfiability

Many problems, in diverse areas such as robotics, software testing, computer-aided design,
machine vision, integrated circuit design, computer networking, and genetics, can be modeled
in terms of propositional satisfiability. Although most of these applications are beyond the
scope of this book, we will study one application here. In particular, we will show how to use
propositional satisfiability to model Sudoku puzzles.

SUDOKU A Sudoku puzzle is represented by a 9 × 9 grid made up of nine 3 × 3 subgrids,
known as blocks, as shown in Figure 1. For each puzzle, some of the 81 cells, called givens,
are assigned one of the numbers 1, 2,..., 9, and the other cells are blank. The puzzle is solved
by assigning a number to each blank cell so that every row, every column, and every one of the
nine 3 × 3 blocks contains each of the nine possible numbers. Note that instead of using a 9 × 9
2
2
2
grid, Sudoku puzzles can be based on n × n grids, for any positive integer n, with the n × n 2
2
grid made up of n n × n subgrids.
The popularity of Sudoku dates back to the 1980s when it was introduced in Japan. It
took 20 years for Sudoku to spread to rest of the world, but by 2005, Sudoku puzzles were a
worldwide craze. The name Sudoku is short for the Japanese suuji wa dokushin ni kagiru, which
means “the digits must remain single.” The modern game of Sudoku was apparently designed
in the late 1970s by an American puzzle designer. The basic ideas of Sudoku date back even
further; puzzles printed in French newspapers in the 1890s were quite similar, but not identical,
to modern Sudoku.
Sudoku puzzles designed for entertainment have two additional important properties. First,
they have exactly one solution. Second, they can be solved using reasoning alone, that is, without
resorting to searching all possible assignments of numbers to the cells. As a Sudoku puzzle is
solved, entries in blank cells are successively determined by already known values. For instance,
in the grid in Figure 1, the number 4 must appear in exactly one cell in the second row. How
can we determine which of the seven blank cells it must appear? First, we observe that 4 cannot
appear in one of the first three cells or in one of the last three cells of this row, because it already
appears in another cell in the block each of these cells is in. We can also see that 4 cannot appear
in the fifth cell in this row, as it already appears in the fifth column in the fourth row. This means
that 4 must appear in the sixth cell of the second row.
Many strategies based on logic and mathematics have been devised for solving Sudoku
puzzles (see [Da10], for example). Here, we discuss one of the ways that have been developed
for solving Sudoku puzzles with the aid of a computer, which depends on modeling the puzzle as
a propositional satisfiability problem. Using the model we describe, particular Sudoku puzzles
can be solved using software developed to solve satisfiability problems. Currently, Sudoku
puzzles can be solved in less than 10 milliseconds this way. It should be noted that there are
many other approaches for solving Sudoku puzzles via computers using other techniques.