为什么在解决8皇后问题时，Z符号的down函数会有一个差异？

Question

我正在读一本名为"The Way of Z: Practical Programming with Formal“的书，在第18章(8皇后问题)中，作者为著名的8皇后问题提供了一个基于Z符号的正式解决方案。他试图通过将对角线部分与直线方程联系起来来解决它。解决方案中使用的变量包括：

​

​

然后，求解对角线部分的直线方程为：

其中file代表这里的一行，rank代表一列。为帮助我们理解对角线而提供的图像是：

​

该解决方案的工作原理如下:文件(行)编号1以蓝色突出显示。等级(列)1以红色突出显示。解决方案是从下到上，从左到右。

我想计算file(row)=4和rank(column)=6 (以黄色突出显示)处的正方形的向上和向下函数值。

所以,

up =排名文件=6-4=2

向下=排名+文件=6+4= 10

如上图所示，上对角线确实在点2处切割y-截距的左边缘，但下对角线在点9(而不是10)处切割y-截距。差值是1，这个差值是所有平方的。我想知道在这种情况下我遗漏了什么？为什么向下箭头的情况总是有所不同(而向上箭头的情况则不同)？

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

​

Answer 1

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

你在问题中提到的书的摘录似乎对这一点不是很清楚，但(据我所知) up() (resp.仅应将皇后的投影与up()进行比较(分别down())，以确定其他皇后区是否位于同一对角线上。否则，这种比较的有效性将是微不足道的可证伪的，例如，给定q1 := Queen(1, 1)和q2 := Queen(6, 4)的，很容易看出down(q1) == up(q2)但q1, q2不会互相攻击。