There is 3x3 grid. Each cell in grid may have a mine or not. For each cell, either it is observed or not. If cell is observed, an indicator for that cell is true iff that cell or one of its diagonally adjacent cells (northeast, northwest, southeast, southwest) has mine in it (note that the "or" here is a standard "disjunctive or", not an "exclusive or").

(a) Describe all binary variables required for propositional encoding of this Minesweeper problem. Provide your propositional variables interpretable names like m 1 2 for variable indicating whether mine is in cell (1, 2). As a function of n, how many variables are required to encode Minesweeper for grid of dimension n × n?

(b) Describe constraints which encode that cell (1, 2) is observed and indicates mine is not present, that cell (2, 1) is observed and indicates a mine is present, and that remaining cells are unobserved.

(c) Describe remaining constraints for this problem need to enforce consistency between all of variables. Note that corner, edge, and middle portions of grid should be treated separately when finding adjacency, e.g., a corner only has one diagonally adjacent cell whereas middle cell (2, 2) has four diagonally adjacent cells. Your constraint encoding must use ) and, and hence must not be in CNF.

(d) Give step-by-step CNF transformation of shortest axiom from (c) which involves the proposition m 1 1.

(e) Encode knowledge base constraints (b) and (c) in DIMACS CNF format explained below. In DIMACS comments, show mapping between variable names and DIMACS variable IDs (e.g., m 1 2 ! 5). Write listing of your DIMACS file. To avoid errors, it is strongly recommended that you write short program or script to generate DIMACS file automatically.