0

我正在尝试使用 SAT Solver 解决扫雷问题。

到目前为止，我了解了游戏的一般逻辑、SAT Solver 的工作原理以及如何实现它。

但是，我不知道如何将我的布尔公式转换为 CNF，以便使用 SAT Solver 解决它。

假设我有以下 5x5 板：

2 XXXX XXXXXX
XXXXX
XXXXXX
XXXXXX

在单元格 1,1 中有值 2，这意味着周围的相邻单元格有 2 个地雷。整个单元格 1,1 有 3 个邻居（单元格 1,2；单元格 2,1；单元格 2,2）。我将调用相邻单元格：1,2 和 3。

这意味着我有以下布尔可能性：

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

如果(a or b) and (c or not d)是一个 CNF，那么 SAT Solver 的语法是：{{1,2},{3,-4}} 其中变量是整数，布尔假值是负整数，真值是正整数。

但是，我不知道如何将扫雷字段的布尔可能性转换为 CNF。

我对有 3 个邻居和 2 个地雷的单元格 1,1 的猜测：

(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)

所以我的 SAT Solver 公式根据语法将是： {{1,2,-3},{1,-2,3},{-1,2,3}}

有人可以确认或更正我的 SAT Solver 公式吗？

谢谢你。

编辑：

经过一番讨论，我想出了以下伪代码想法/方法：

# 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

  • 任何形式的任何评论都将受到高度赞赏和帮助。

  • 此外，一旦我检查并遍历每个单元格，这种方法会解决游戏吗？

谢谢你。

4

0 回答 0