CompSci 102 Discrete Mathematics for CSSpring 2005 Forbes MinesweeperFrom Umesh Varirani’s notes!CNFIn the area of logical reasoning systems, conjunctive normal form (CNF) is much more commonlyCONJUNCTIVENORMAL FORMused. In CNF, every expression is a conjunction of disjunctions of literals. A disjunction of literalsis called a clause. For example, the following expression is in CNF:CLAUSE(¬A ∨ B) ∧ (¬B ∨ ¬C) ∧ (A ∨ C ∨ D)We can easily show the following result:Theorem 25.1: For every Boolean expression, there is a logically equivalent CNF expression.Proof: Any Boolean expression B is logically equivalent to the c onjunction of the negation of eachrow of its truth table with value F . The negation of each row is the negation of a conjunction ofliterals, which (by de Morgan’s law) is equivalent to a disjunction of the negations of literals, whichis equivalent to a disjunction of literals. 2Another way to find a CNF expression logically equivalent to any given expression is througha recursive transformation process. This does not require constructing the truth table for theexpression, and can result in much smaller CNF expressions.The steps are as follows:1. Eliminate ⇔ , replacing A ⇔ B with (A ⇒ B) ∧ (B ⇒ A).2. Eliminate ⇒ , replacing it A ⇒ B with ¬A ∨ B.3. Now we have an expression containing only ∧, ∨, and ¬. The conversion of ¬CNF(A) intoCNF, where CNF(A) is the CNF equivalent of expression A, is extremely painful. Therefore,we prefer to “move ¬ inwards” using the following operations:¬(¬A) ≡ A¬(A ∧ B) ≡ (¬A ∨ ¬B) (de Morgan)¬(A ∨ B) ≡ (¬A ∧ ¬B) (de Morgan)Repeated application of these operations res ults in an expression containing nested ∧ and ∨operators applied to literals. (This is an easy proof by induction, very similar to the NANDproof.)4. Now we apply the distributivity law, distributing ∧ over ∨ wherever possible, resulting in aCNF expression.We will now prove formally that the last step does indeed result in a CNF expression, as stated.1Theorem 25.2: Let B be any Boolean expression constructed from the operators ∧, ∨, and ¬,where ¬ is applied only to variables. Then there is a CNF expression logically equivalent to B.Obviously, we could prove this simply by appealing to Theorem 6.4; but this would leave us withan algorithm involving a truth-table construction, which we wish to avoid. Let’s see how to do itrecursively.Proof: The proof is by induction over Boolean expressions on the variables X. Let P (B) be theproposition that B can be expressed in CNF; we assume B contains only ∧, ∨, and ¬, where ¬ isapplied only to variables.• Base case: prove P(T ), P (F ), and ∀X ∈ X P (X) and ∀X ∈ X P (¬X).These are true since a conjunction of one disjunction of one literal is equivalent to the literal.• Inductive step (∧): prove ∀B1, B2∈ B [P (B1) ∧ P (B2) ⇒ P (B1∧ B2)].1. The inductive hypothesis s tates that B1and B2can be expressed in CNF. Let CNF (B1)and CNF (B2) be two such expressions.2. To prove: B1∧ B2can be expressed in CNF.3. By the inductive hypothesis, we haveB1∧ B2≡ CNF (B1) ∧ CNF (B2)≡ (C11∧ . . . ∧ Cm1) ∧ (C12∧ . . . ∧ Cn2) (Cijs are clauses)≡ (C11∧ . . . ∧ Cm1∧ C12∧ . . . ∧ Cn2)4. Hence, B1∧ B2is equivalent to an expression in CNF.• Inductive step (∨): prove ∀B1, B2∈ B [P (B1) ∧ P (B2) ⇒ P (B1∨ B2)].1. The inductive hypothesis s tates that B1and B2can be expressed in CNF. Let CNF (B1)and CNF (B2) be two such expressions.2. To prove: B1∨ B2can be expressed in CNF.3. By the inductive hypothesis, we haveB1∨ B2≡ CNF (B1) ∨ CNF (B2)≡ (C11∧ . . . ∧ Cm1) ∨ (C12∧ . . . ∧ Cn2) (Cijs are clauses)≡ (C11∨ C12) ∧ (C11∨ C22) ∧ . . . ∧ (Cm1∨ Cn−12) ∧ (Cm1∨ Cn2)4. By associativity of ∨, each expression of the form (Ci1∨ Cj2) is equivalent to a singleclause containing all the literals in the two clauses.5. Hence, B1∨ B2is equivalent to an expression in CNF.Hence, any Boolean expression constructed from the operators ∧, ∨, and ¬, where ¬ is applied onlyto variables, is logically equivalent to an expression in CNF. 2This process therefore “flattens” the logical expression, which might have many levels of nesting,into two levels. In the process, it can enormously enlarge it; the distributivity step converting DNFinto CNF can give an exponential blowup when applied to nested disjunctions (see below). As withthe conversion to NAND-form, the proof gives a recursive conversion algorithm directly.Many problems of interest in CS can be converted into CNF representations; solved using theorem-proving algorithms for CNF; and then the solution is translated back into the original language ofthe problem. Why would we do this?CompSci 102, Spring 2005, Minesweeper 2mines left: 6 mines left: 0 mines left: 1 mines left: 243211 2 3 44 m 2 2 m3 3 4 m 22 m m 2 11 m 3 1 01 2 3 421 1 1 11 2 321 1 1 1 1 11 2 3 4 5(a) (b) (c) (d)Figure 1: Minesweeper examples. (a) Initial display for a 4 × 4 game. (b) Final display aftersuccessful discovery of all mines. (c) Simple case: only one solution. (d) Two possible solutions,but both have (3,1) blank.• Because we can work on finding efficient algorithms for CNF instead of finding efficient algo-rithms for hundreds of different problems.• Because we can take advantage of all the work other people have done in finding efficientalgorithms for CNF.• Because often we find, once we reach CNF, that we have one or other special case of CNF forwhich very efficient (e.g., linear-time) algorithms are known.There are other “canonical problem” targets besides CNF, including matrix inversion and determi-nants, linear programming, and finding roots of polynomials. As one becomes a good computerLINEARPROGRAMMINGscientists, one develops a mental “web” of interrelated standard computational problems and learnsto map any new problem onto this web. Minesweeper is a good example.MinesweeperThe rules of Minesweeper are as follows:• The game is played by a single player on an X × Y board. (We will use Cartesian coordinates,so that (1,1) is at bottom left and (X,1) is at bottom right.) The display is initially empty.The player is told the total number of mines remaining undiscovered; these are distributeduniformly at random on the board. (See Figure 1(a).)• At each turn the player has three options:1. Mark a square as a mine; the display is updated
View Full Document
Unlocking...