1

我正在阅读名为“The Way of Z: Practical Programming with Formal Methods by Jonathan Jacky”的书，在第 18 章（8 Queen 问题）中，作者为著名的 8 Queen 问题提供了基于 Z 符号的正式解决方案。他试图通过将它连接到一个直线方程来求解对角线部分。解决方案中使用的变量是：

变量

那么求解对角线部分的直线方程为： 线方程 其中file在这里代表一行，rank代表一列。为帮助我们理解对角线而提供的图像是： 对角线图像

该解决方案的工作原理如下：文件（行）编号 1 以蓝色突出显示。rank(column) 1 以红色突出显示。解决方案从下到上，从左到右。

我想计算 file(row)=4 和 rank(column)=6 的正方形的 up 和 down 函数值（以黄色突出显示）。

所以，

向上 = 等级 - 文件 = 6 - 4 = 2

下降 = 等级 + 文件 = 6 + 4 = 10

如上图所示，上对角线确实在点 2 处切割 y 截距的左边缘。但下对角线在点 9（而不是 10）处切割 y 截距。有 1 的差异。这个差异适用于所有正方形。我想知道在这种情况下我缺少什么？为什么在向下箭头的情况下（而不是在向上箭头的情况下）总是存在差异？

我还附上了完整的基于 Z 符号的解决方案以供参考： 完整解决方案

4

1 回答 1

1

图片中描述的投影和文本中的投影不同，但这似乎并不重要：唯一需要维护的属性是1.up()/down()两个皇后在同一对角线上的投影是相同的2 .两个皇后在不同对角线上的up()/down()投影是不同的。

您在问题中提出的书的摘录似乎对此并不太清楚，但是（据我所知）女王的up()（resp。down()）投影应该只与up()（resp。down()）其他皇后的投影，以确定它们是否位于同一对角线上。否则，这种比较的有效性将很容易被证伪，例如， 给定 aq1 := Queen(1, 1)和q2 := Queen(6, 4)，很容易看出这一点，down(q1) == up(q2)但q1, q2不要互相攻击。

于 2020-05-10T09:21:38.363 回答