🔢 mathematics

Queen Domination by SAT Solving

本文提出了一种高性能、可生成证明的 SAT 框架，该框架通过利用几何启发式编码、对称性破缺以及确保可独立验证正确性的统一验证流水线，解决了此前悬而未决的 $n=19$ 后皇后支配问题，并修正了 $n=16$ 的枚举结果。

原作者： Taha Rostami, Curtis Bright

发布于 2026-07-30

📖 1 分钟阅读🧠 深度阅读

原作者： Taha Rostami, Curtis Bright

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一个数学不再仅仅是纸上的数字，而是关于解决那些甚至会让最聪明的人类大脑都感到眩晕的复杂谜题的世界。这就是组合搜索（combinatorial search）的领域，它是计算机科学和数学的一个分支，致力于寻找排列事物的最佳方式。你可以把它想象成试图为一个盛大的婚礼制定完美的座位表，每个宾客对于谁可以坐在自己旁边都有特定的规则；或者是在计算为了监视博物馆的每个角落且不留下盲点，究竟最少需要多少名保安。

这个领域中最著名的谜题之一是皇后支配问题（Queen Domination Problem）。想象一个国际象棋棋盘。皇后是一个强大的棋子，它可以攻击其所在行、列以及两条对角线路径上的所有位置。问题看似简单实则棘手：你需要在 $n \times n$ 的棋盘上放置最少数量的皇后，使得每一个方格都处于被攻击的状态，请问这个最小数量是多少？对于小棋盘来说，这听起来很容易，但随着棋盘变大，可能的排列组合数量会爆炸式增长，达到数十亿、数万亿甚至更多。一个多世纪以来，数学家们一直试图解决这个问题，不仅是为了找到那个数字，更是为了精确计算出有多少种不同的排列方式。为什么这很重要？因为解决这些谜题有助于我们理解如何组织复杂的系统，从调度航班到设计计算机芯片。但这里有一个陷阱：当计算机进行数学运算时，它们可能会出错，有时甚至会完全错过答案。

这就是 Taha Rostami 和 Curtis Bright 在其论文《通过 SAT 求解器实现皇后支配》（Queen Domination by SAT Solving）中切入的地方。他们致力于解决的问题是：计算在高达 19 阶的棋盘上，用最少数量的皇后实现支配的所有唯一排列方式。他们并没有像之前的研究人员那样编写专门的程序去搜寻解法，而是将整个国际象棋谜题翻译成了一种 SAT 求解器（一种超智能逻辑机器）能够理解的语言。你可以把 SAT 求解器想象成一名侦探，它负责检查一组规则是否可能成立。如果侦探说“不”，它可以提供一份任何人都可以核查的证明证书，以确保侦探没有撒谎。

作者们构建了一个特殊的棋盘“翻译”版本，该版本突出了游戏的几何特性，并使用了一种被称为希尔伯特曲线（Hilbert curve）的巧妙技巧来组织线索，以便让侦探更快地找到答案。他们还使用了一种名为 Cube-and-Conquer 的策略，这就像是将一个巨大且无法独自吞下的蛋糕，切成成千上万个微小且易于处理的小块，让不同的计算机可以同时“食用”。结果如何？他们不仅解决了谜题，还证明了他们的解法是 100% 正确的。

他们的工作揭示了该问题历史上一个令人惊讶的错误。对于一个 16x16 的棋盘，之前的专家认为只有 43 种唯一的皇后放置方式。而 Rostami 和 Bright 证明了实际上有 371 种方式——这是一个巨大的差异，表明旧的计算机程序存在隐藏的漏洞，导致遗漏了大部分解法。此外，他们还解决了一个长期悬而未决的案例：19x19 的棋盘。他们发现，要用最少数量的皇后支配该棋盘，恰好有 11 种唯一的方式。通过为每一个结果生成“证明证书”，他们为数学界提供了前所未有的信任水平，证明了当我们将智能编码与严谨的证明检查相结合时，即使是最好的专用软件也可能错失的难题，我们也能迎刃而解。

技术摘要：通过 SAT 求解实现皇后支配问题

问题定义
皇后支配问题旨在寻找能够攻击 $n \times n$ 棋盘上所有方格的最少皇后数量，记作 $\gamma(Q_n)$ 。除了确定该最小值外，一个重大的挑战在于对所有在同构意义下（考虑旋转和反射等棋盘对称性）的互不相同的解进行枚举。虽然使用 UNIDOM 等专门搜索工具已确定了 $n \le 25$ 的最优值 $\gamma(Q_n)$ ，但对于更大规模棋盘的非同构解枚举仍然具有极高的计算强度。在这一领域，计算结果的可靠性是一个关键问题；以往在其他组合证明中出现的差异（例如 Lam 问题）以及专门求解器中发现的漏洞，凸显了对独立可验证正确性证书的需求。

方法论
作者提出了一种用于解决皇后支配问题的生成证明型布尔可满足性（SAT）框架。该方法并非实现自定义搜索算法，而是将问题编码为合取范式（CNF）形式的命题公式。该方法依赖于以下几项关键技术创新：

直线变量编码（Line-Variable Encoding）： 核心创新是引入了表示特定几何直线（行、列、对角线和反对角线）是否至少包含一个皇后的辅助布尔变量。
- 皇后变量 ( $Q_i$ )：指示是否在方格 $i$ 放置了皇后。
- 直线变量 ( $L_\ell$ )：指示直线 $\ell$ 是否是“活跃”的（即包含一个皇后）。
- 约束条件：子句确保如果一条直线是活跃的，则该直线上必须存在一个皇后。支配问题通过要求每个方格至少与其相交的四条直线之一处于活跃状态来表达。基数约束限制了皇后的总数 ( $\sum Q_i \le \gamma$ ) 以及活跃直线的总数 ( $\sum L_\ell \le 4\gamma$ )。
基数编码与文字排序（Cardinality Encoding and Literal Ordering）：
- 基数约束使用基于 Totalizer 的方法进行编码。皇后约束使用与 Cube-and-Conquer 框架兼容的标准 Totalizer，而直线约束则使用模 Totalizer 以提升性能。
- 希尔伯特曲线排序（Hilbert Curve Ordering）： 在皇后基数约束中应用了一种新颖的文字排序策略。通过希尔伯特曲线遍历棋盘，将空间相邻的方格组合在计数树中。这保留了空间局部性，从而实现了更强的单位传播（unit propagation）。实验表明，这种排序处理 $n=14$ 的实例时，比默认排序快约 31.5 倍。
对称性破缺（Symmetry Breaking）： 为了消除对对称解的冗余探索，该框架在原始皇后配置及其七个非恒等几何变换之间强制执行字典序约束（基于 Warwick Harvey 的方法）。在初步测试中，这显著降低了求解时间（例如 $n=15$ 时实现了 6.64 倍的加速）。
Cube-and-Conquer： 对于较大的实例，通过在 Totalizer 编码的辅助变量上进行分支，将搜索空间划分为独立的子问题（cubes）。这允许并行求解并提高了可扩展性，且无需依赖于单个皇后的放置来进行划分。
证明生成与验证： 该框架使用 cadical-exhaust 通过迭代添加阻塞子句来枚举所有模型。它生成带有“信任子句”（trusted clauses）的 DRAT 证明，以证明其完备性。这些证明使用 drat-trim-t 进行独立验证，确保结果不依赖于求解器内部搜索逻辑的正确性，而仅依赖于编码和证明检查器。

关键结果
该研究成功枚举了所有 $n \le 19$ 的非同构最小皇后支配解。结果包括：

文献修正： 对于 $n=16$ ，本文指出了先前报告中的一项差异。虽然专门的求解器 UNIDOM 报告了 43 个非同构解，但本 SAT 框架证明实际恰好有 371 个。作者将其归因于 UNIDOM 中的一个漏洞，该漏洞会导致在特定配置下遗漏有效的解。
解决开放案例： 之前悬而未决的 $n=19$ 案例得到了解决，确定其恰好有 11 个非同构最小解。
性能： 在非平凡实例上，该 SAT 框架的表现始终优于专门的求解器 UNIDOM。对于 $n=19$ ，采用 SAT 方法的枚举耗时约为 171,575 秒（CPU 时间），而 UNIDOM 为 714,733 秒。引入直线变量至关重要；一个不含直线变量的初步版本在求解和验证 $n=19$ 实例时，耗时增加了 22.8 倍。

意义与主张
本文声称，其主要贡献在于为皇后支配枚举问题提供了一个高性能且可独立验证的解决方案。通过从专门的搜索代码转向生成证明型的 SAT 框架，作者降低了对计算过程所需的“信任度”。结果的正确性现在仅取决于 SAT 编码和外部证明验证器，而非专门求解器复杂的自定义逻辑。

这项工作证明，精心的编码设计——特别是引入辅助变量以揭示几何结构、使用全局约束以及具备几何感知能力的文字排序——可以使生成证明型的 SAT 求解在竞争力和性能上超越高度优化的领域特定求解器。作者公开了其源代码和解数据，以促进进一步的验证与研究。

技术摘要：通过 SAT 求解实现皇后支配问题

类似论文