我有一个学校项目，我必须在其中找到游戏的解决方案。求解器，但我遇到了麻烦，试图设置游戏的联合正常形式。
游戏由5 x 5个灯光组成。按下任何灯都会对其进行切换和四个相邻的灯。难题的目的是关闭所有灯。
我到目前为止的尝试：
对于3x3网格（首先），我设置了9个术语（对于每个按钮），因此：
c11：位置1,1处的按钮变浅C12：位置1,2处的按钮变浅C13：位置1,3处的按钮将减轻。[...]
由于位于1,2和2,1
的1,1处按钮的按钮关闭按钮我做了C11 => C12和C21在1,1和1,3和2,2处的按钮处的1,2灯在1,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
您发布的Wikipedia文章引用了一些看起来不错的解决方案：Marlow Anderson，Todd Feil（1998）。"用线性代数旋转灯"（PDF）。数学杂志。71（4）：300–303。您将需要了解论文中的数学以及如何将Z_2操作编码为CNF。（IMO的实施工作要比BMC少。
解决问题的一种方法是编码达到目标所需的动作顺序。
做到这一点的一种方法是考虑k的动作来解决难题。然后，您将为选择单元格的每个步骤编码，以及对相关单元格的影响，并询问求解器的模型，以使k-th配置都关闭了所有点亮。
此技术称为有界模型检查，您应该找到有关如何转换为SAT的一些解释。