n-Queens Problem：为何约束表达式为真时可断言每行最多1个皇后？

先明确基础建模约定 #

所有n皇后的约束求解，第一步都是给棋盘格子绑定可计算的变量：

• 对棋盘上第i行、第j列的格子，定义布尔变量q[i][j]：取值为True代表该格子摆放皇后，取值为False代表该格子不摆放皇后。
• 所有被要求为True的约束表达式，本质都是把皇后的走棋规则，翻译成计算机能自动校验的逻辑判断，没有脱离实际规则的抽象设定。

「每行最多1个皇后」的约束逻辑本质 #

很多初学者刚接触建模时，容易把“行约束”的两层要求搞混：行层面的要求其实拆成了两个独立部分，一个是「每行至少1个皇后」，一个是「每行最多1个皇后」，我们单说“最多1个”的逻辑：
所谓“最多1个皇后”，对应的现实规则非常直白：同一行里如果放了2个及以上皇后，这些皇后可以横向直接攻击到对方，是绝对不允许的。
把这个规则翻译成能计算的逻辑表达式，逻辑是非常直接的：

对固定的某一行i，我们从这一行里任意挑选两个不同列的位置j1、j2，这两个位置绝对不允许同时摆放皇后。

这个禁止要求写成标准布尔逻辑就是：对同一行内所有满足j1 ≠ j2的列组合，必须满足表达式 ¬q[i][j1] ∨ ¬q[i][j2] 的取值为True。

你可以逐种情况代入验证这个表达式的约束效果：

• 如果该行没有放任何皇后：所有q[i][j]都是False，对应的两个否定命题都是True，整个析取式自然为True，符合要求
• 如果该行恰好放了1个皇后：该行剩下的所有位置都是False，随便挑两个位置校验，要么两个都是空的，要么一个有皇后一个是空的，对应的否定命题至少有一个是True，整个析取式也为True，符合要求
• 如果该行放了2个及以上皇后：我们只要挑那两个实际摆了皇后的位置j1、j2，对应的两个否定命题都是False，整个析取式直接为False——刚好违反了“约束必须为True”的要求，会被求解机制直接判定为非法布局。

为什么你看到的表达式会直接绑定“最多1个”的判断 #

你在参考图里看到的行约束，大概率是建模时做了简化合并的写法：

• 很多教程不会把所有两两组合的析取式单独列出来，而是会把同一行所有q[i][j]的取值当成0/1数（True为1，False为0）求和，把“恰好1个皇后”的两个要求（既不能少于1个，也不能多于1个）合并成一个等式：对固定行i，所有列位置的q[i][j]求和结果必须等于1。
• 当我们要求这个等式恒为True时，变量的取值天然不可能出现总和大于1的情况，自然就直接实现了“每行最多1个皇后”的断言；同理，求和结果也不可能小于1，也就同时满足了“每行至少1个皇后”的要求。
• 如果看到的是不等式形式的约束，比如对固定行i，sum(q[i][j] for j in 1..n) <= 1，那这个式子被要求为True时，就是纯粹的“每行最多1个皇后”的约束——因为求和结果被卡死在1以内，根本不可能出现两个皇后的解。

常见的理解误区 #

很多人推导的时候卡壳，是上来就盯着抽象的逻辑符号看，忘了回头锚定一下变量和实际棋盘格子的对应关系。只要记得每个逻辑表达式都是对某条棋盘规则的直接翻译，不需要绕复杂的推导，所有约束的逻辑都是顺的。

内容的提问来源于stack exchange，提问作者Jie