Reputation: 109
I'm trying to solve Minesweeper with a SAT Solver.
So far i understand the general logic of the game, how the SAT Solver works and how to implement it.
However i can't wrap my head around, how to translate my boolean formula into a CNF in order to solve it with a SAT Solver.
lets say i have the following 5x5 Board:
2 X X X X
X X X X X
X X X X X
X X X X X
X X X X X
In cell 1,1 there is value 2, which means the surrounding neighbor cells have 2 mines. Overall cell 1,1 has 3 neighbors (cell 1,2; cell 2,1; cell 2,2). I will call the neighbor cells: 1,2 and 3.
That means i have the following boolean possibilities:
cell 1 = Bomb
cell 2 = Bomb
cell 3 = No Bomb
or
cell 1 = Bomb
cell 2 = No Bomb
cell 3 = Bomb
or
cell 1 = No Bomb
cell 2 = Bomb
cell 3 = Bomb
If (a or b) and (c or not d) is a CNF than the syntax for a SAT Solver is: {{1,2},{3,-4}} where the variables are integers and the boolean false values are negative integers and the true values are positive integers.
However, I don't know how to turn my boolean possibilities of the minesweeper field into a CNF.
My guess for cell 1,1 with 3 neighbors and 2 mines:
(Bomb 1,2 or Bomb 2,1 or no Bomb 2,2) and
(Bomb 1,2 or no Bomb 2,1 or Bomb 2,2) and
(no Bomb 1,2 or Bomb 2,1 or Bomb 2,2)
so my SAT Solver formula according to the syntax would be: {{1,2,-3},{1,-2,3},{-1,2,3}}
Can someone please confirm or correct my SAT Solver formula?
Thank you.
Edit:
After some discussion, i came up with the following pseudo code idea/approach:
# pseudo code for cell_x_y_n of corner type (3 neighbors) with n = 2 bombs
for cell_x_y in minesweeper_board:
if cell_x_y == corner_cell and cell_value_n == 2:
check with SAT Solver if knowledge_base(cell_x_y_2) ∪ bomb_x_y is satisfiable:
if satisfiable == True:
mark cell_x_y as bomb and don't visit anymore
continue
if satisfiable == False:
cell_x_y has no bomb and don't visit anymore
continue
Any remarks of any kind are highly appreciated and helpful.
Also once i checked and looped through every cell will this approach solve the game?
Thank you.
Upvotes: 0
Views: 420