SKEDSOFT

Propositional Satisfiability: Acompound proposition is satisfiable if there is an assignment of truth values to its variables that makes it true. When no such assignments exists, that is, when the compound proposition is false for all assignments of truth values to its variables, the compound proposition is unsatisfiable.

Note that a compound proposition is unsatisfiable if and only if its negation is true for all assignments of truth values to the variables, that is, if and only if its negation is a tautology. When we find a particular assignment of truth values that makes a compound proposition true, we have shown that it is satisfiable; such an assignment is called a solution of this particular satisfiability problem. However, to show that a compound proposition is unsatisfiable, we need to show that every assignment of truth values to its variables makes it false. Although we can always use a truth table to determine whether a compound proposition is satisfiable, it is often more efficient not to, as Example 1 demonstrates.

EXAMPLE 1 Determine whether each of the compound propositions (p ∨¬q) ∧ (q ∨¬r) ∧ (r ∨¬p), (p ∨ q ∨ r) ∧ (¬p ∨¬q ∨¬r), and (p ∨¬q) ∧ (q ∨¬r) ∧ (r ∨¬p) ∧ (p ∨ q ∨ r) ∧ (¬p ∨¬q ∨¬r) is satisfiable.

Solution: Instead of using truth table to solve this problem, we will reason about truth values. Note that (p ∨¬q) ∧ (q ∨¬r) ∧ (r ∨¬p) is true when the three variable p, q, and r have the same truth value (see Exercise 40 of Section 1.1). Hence, it is satisfiable as there is at least one assignment of truth values for p, q, and r that makes it true. Similarly, note that (p ∨ q ∨ r) ∧ (¬p ∨¬q ∨¬r) is true when at least one of p, q, and r is true and at least one is false (see Exercise 41 of Section 1.1). Hence, (p ∨ q ∨ r) ∧ (¬p ∨¬q ∨¬r) is satisfiable, as there is at least one assignment of truth values for p, q, and r that makes it true.

Finally, note that for (p ∨¬q) ∧ (q ∨¬r) ∧ (r ∨¬p) ∧ (p ∨ q ∨ r) ∧ (¬p ∨¬q ∨¬r) to be true, (p ∨¬q) ∧ (q ∨¬r) ∧ (r ∨¬p) and (p ∨ q ∨ r) ∧ (¬p ∨¬q ∨¬r) must both be true. For the first to be true, the three variables must have the same truth values, and for the second to be true, at least one of three variables must be true and at least one must be false. However, these conditions are contradictory. From these observations we conclude that no assignment of truth values to p, q, and r makes (p ∨¬q) ∧ (q ∨¬r) ∧ (r ∨¬p) ∧ (p ∨ q ∨ r) ∧ (¬p ∨¬q ∨¬r) true. Hence, it is unsatisfiable

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 grid, Sudoku puzzles can be based on n2 × n2 grids, for any positive integer n, with the n2 × n2 grid made up of n2 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. we can determine seven blank cells in which 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.

To encode a Sudoku puzzle, let p(i, j, n) denote the proposition that is true when the number n is in the cell in the ith row and j th column. There are 9 × 9 × 9 = 729 such propositions, as i, j , and n all range from 1 to 9. For example, for the puzzle in Figure 1, the number 6 is given as the value in the fifth row and first column. Hence, we see that p(5, 1, 6) is true, but p(5, j, 6) is false for j = 2, 3, . . . , 9.

Given a particular Sudoku puzzle, we begin by encoding each of the given values. Then, we construct compound propositions that assert that every row contains every number, every column contains every number, every 3 × 3 block contains every number, and each cell contains no more than one number. It follows, as the reader should verify, that the Sudoku puzzle is solved by finding an assignment of truth values to the 729 propositions p(i, j, n) with i, j , and n each ranging from 1 to 9 that makes the conjunction of all these compound propositions true. After listing these assertions, we will explain how to construct the assertion that every row contains every integer from 1 to 9.We will leave the construction of the other assertions that every column contains every number and each of the nine 3 × 3 blocks contains every number to the exercises.