0

我有一个学校项目，我必须使用 SAT Solver 找到游戏“Lights Out”（https://en.wikipedia.org/wiki/Lights_Out_(game)）的解决方案，但我在尝试设置连接词时遇到了麻烦游戏的正常形式。

游戏由 5 x 5 的灯光网格组成。按下任何一个灯都会切换它和四个相邻的灯。谜题的目标是关掉所有的灯。

到目前为止我是如何尝试的：

对于 3x3 网格（开始），我设置了 9 个术语（每个按钮），因此：

C11 : 位置 1,1 的按钮变亮 C12 : 位置 1,2 的按钮变亮 C13 : 位置 1,3 的按钮变亮。[...]

由于 1,1 处的按钮熄灭 1,2 和 2,1 位置处的按钮

我做了 C11 => C12 和 C21 1,2 处的按钮熄灭了位置 1,1 和 1,3 和 2,2 我做了 C12 => C11 和 C13 和 C22

并继续另一个：

C13 => C12 and C23
C21 => C11 and C22 and C31
C22 => C12 and C21 and C23 and C32
C23 => C13 and C22 and C33
C31 => C21 and C32
C32 => C31 and C33 and C22
C33 => C23 and C32

然后我只是将这些转换为 CNF 以获得 sat 求解器所需的子句，但似乎我做错了..

谁能帮我把这个游戏写成 CNF 形式？

非常感谢 ！

如果您需要更好地理解它，这里是游戏：

https://www.geogebra.org/m/JexnDJpt#material/KArehWn8

4

2 回答 2

2

您发布的维基百科文章引用了一些看起来不错的解决方案：Marlow Anderson, Todd Feil (1998)。“用线性代数关灯”（PDF）。数学杂志。71（4）：300-303。您将需要了解论文中的数学以及如何将 Z_2 操作编码为 CNF。（IMO 的实施工作比 BMC 少。）祝你好运！

于 2019-02-27T23:45:12.103 回答
1

解决问题的一种方法是对实现目标所需的操作序列进行编码。

这样做的一种方法是考虑需要 K 步来解决这个难题。然后，您将为每个步骤对选择单元格以及对相关单元格的影响进行编码，并要求求解器提供一个模型，以使第 K 个配置的所有灯都熄灭。

这种技术称为有界模型检查，您应该找到一些关于如何转换为 sat 的解释。

于 2019-02-27T20:32:50.957 回答