philuix
philuix

Reputation: 109

How to translate a boolean formula into CNF for a SAT Solver?

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

Thank you.

Upvotes: 0

Views: 420

Answers (0)

Related Questions