SAT + NAUTY: Orderly Generation of Small Kochen-Specker Sets Containing the Smallest State-independent Contextuality Set

这是一份关于论文《SAT + NAUTY: Orderly Generation of Small Kochen-Specker Sets Containing the Smallest State-independent Contextuality Set》（SAT + NAUTY：包含最小状态无关语境性集合的小规模 Kochen-Specker 集合的有序生成）的详细技术总结。

1. 研究背景与问题定义

核心问题：
在三维希尔伯特空间（$d=3$）中，寻找最小的 Kochen-Specker (KS) 集合。

• KS 集合定义：一组有限射线，无法进行 $\{0, 1\}$ 赋值，使得每个正交基恰好有一个 1，且每对正交射线中至多一个为 1。
• 状态无关语境性 (SI-C) 集合：一种特殊的 KS 集合，其对应的非语境不等式被任何初始量子态违反。
• 已知事实：
  • 最小的 SI-C 集合是 Yu-Oh 13 射线集（由所有坐标为 $\{0, 1, -1\}$ 的实向量组成）。
  • 最小的已知 KS 集合是 Conway-Kochen 的 31 射线集。
  • 已知下界：KS 集合至少需要 24 条射线。
  • 具体目标：研究从 Yu-Oh 13 射线集出发，通过递归添加正交射线生成的刚性（Rigid）KS 集合。已知存在一个包含 25 条射线的“完整 SI-C 核心”（Complete SI-C Set），它是 Yu-Oh 集在正交闭包操作下的唯一闭包。
  • 挑战：Schütte 发现了一个包含该 25 射线核心的 33 射线 KS 集合。研究目标是穷举所有包含该 25 射线核心、且射线数不超过 33 的 KS 集合，以验证 Schütte 集合是否为唯一解。

技术难点：

• 搜索空间巨大：从 25 条射线扩展到 33 条射线的组合空间极其庞大。
• 同构消除瓶颈：在有序生成（Orderly Generation）中，必须排除同构图。传统的基于字典序（Lexicographical）的规范形式检查在大规模图（$n \ge 25$）上表现出指数级的时间复杂度，导致搜索无法进行。

---

2. 方法论 (Methodology)

作者提出了一种名为 SAT + NAUTY 的新框架，结合了 SAT 求解器的逻辑推理能力与 NAUTY 工具的高效同构检测能力。

2.1 核心创新：递归规范标记 (Recursive Canonical Labeling, RCL)

• 问题：NAUTY 生成的规范标记虽然高效，但不具备遗传性（Hereditary）（即：大图是规范的，其子图不一定是规范的）。这导致无法直接在 SAT 求解器的搜索树中进行剪枝（因为剪枝需要前缀性质）。
• 解决方案：采用 Afzaly (2016) 提出的 RCL 技术。
  • 将 NAUTY 作为基础规范函数 $\delta$。
  • 通过递归构建：对于 $k$ 个顶点的子图，先找到 $k-1$ 个顶点的规范子图，再根据 NAUTY 的结果确定第 $k$ 个顶点的标签。
  • 结果：构建出一种既具备 NAUTY 的高效性，又满足有序生成所需的**遗传性（前缀保持）**的规范形式。

2.2 SAT 编码与求解流程

• 变量定义：
  • $e_{i,j}$：表示顶点 $i$ 和 $j$ 是否正交（边是否存在）。
  • $t_{i,j,k}$：表示 $i, j, k$ 是否构成正交三元组。
• 约束条件：
  1. 结构约束：无 4 环（Squarefree）、最小度 $\ge 3$、每个顶点至少属于一个三角形。
  2. 非 010-可着色性：KS 集合的核心性质。通过生成阻断子句（Blocking Clauses）来排除所有合法的 010-着色方案。
  3. 固定子图：强制前 25 条射线（完整 SI-C 核心）的结构固定。
• 求解器集成：
  • 使用 CaDiCaL SAT 求解器。
  • 通过自定义传播器（Propagator）集成 RCL 检查。每当求解器完成一个前缀子图 $G[k]$ 的赋值时，立即调用 RCL 检查。
  • 若 $G[k]$ 非规范，则添加阻断子句，强制回溯。

2.3 几何可行性检查 (Orthogonality Check)

• 动态坐标推导：利用几何知识，当新射线 $v$ 被约束与两个已知正交向量 $u_1, u_2$ 正交时，其方向由叉积 $\vec{v} = \vec{u}_1 \times \vec{u}_2$ 唯一确定。
• 冲突检测：
  • 检测是否生成平行向量。
  • 检测是否违反正交性（点积不为 0）。
• 依赖链阻断：当发现几何矛盾时，不阻断整个赋值，而是计算导致矛盾的最小依赖链（Edge Dependency Chain），仅阻断导致该矛盾的具体边选择，保留搜索空间的其他有效部分。
• 精确算术：使用 Z3 和代数域进行精确计算，避免浮点误差。

2.4 可验证性 (Verification)

• 扩展了 DRAT 证明格式，支持两类特定子句：
  • t-clauses：同构阻断子句。
  • o-clauses：几何矛盾阻断子句。
• 提供了一个独立的验证器，用于验证这些子句的合法性，确保没有遗漏任何有效的 KS 集合。

---

3. 主要贡献 (Key Contributions)

1. SAT + NAUTY 框架：首次成功将高效的图同构工具 NAUTY 嵌入到 SAT 求解器的有序生成流程中，解决了传统字典序方法在大规模结构化图上的扩展性瓶颈。
2. 递归规范标记 (RCL) 的实现：证明了 RCL 可以在保持 NAUTY 毫秒级性能的同时，满足有序生成所需的遗传性剪枝条件。
3. 几何感知的 SAT 求解：将几何约束（向量坐标、叉积）直接集成到 SAT 传播器中，实现了组合搜索与几何可行性的同步剪枝。
4. 可验证的穷举证明：生成了长达 13 TiB 的独立可验证证明证书，确保了穷举搜索结果的绝对可靠性。

---

4. 实验结果 (Results)

4.1 性能对比

• 基准测试：在 15 到 26 个顶点的规范图上测试。
• 字典序 (Lex) vs. RCL：
  • 在 $n=15$ 时，两者性能相当。
  • 随着 $n$ 增加，字典序检查时间呈指数级增长（$n=26$ 时平均耗时约 3.8 分钟）。
  • RCL 检查时间保持恒定（约 27 毫秒）。
  • 加速比：在 $n=26$ 时，RCL 比字典序快 8,499 倍。
• 结论：对于 KS 集合生成这种高度结构化的问题，字典序方法完全不可行，RCL 是必须的。

4.2 穷举搜索结果

• 搜索范围：包含完整 25 射线 SI-C 核心，射线数从 25 到 33 的所有 KS 集合。
• 计算资源：1,641 个 CPU 小时（约 68 天），在 128 核集群上并行运行。
• 发现：
  • 求解器找到了 44 个满足组合条件的非同构候选图。
  • 经过几何嵌入检查，只有 1 个候选图在 $\mathbb{R}^3$ 或 $\mathbb{C}^3$ 中是几何可实现的。
  • 该唯一解同构于 Schütte 33 射线集。
• 结论：在 33 条射线以内，Schütte 集合是唯一包含完整 25 射线 SI-C 核心的 Kochen-Specker 集合。

---

5. 意义与影响 (Significance)

1. 量子基础理论的突破：

   • 确认了 Schütte 集合在包含最小 SI-C 核心（Yu-Oh 集）的刚性扩展中的唯一性。
   • 为三维空间中“最简单的语境结构”划定了明确的几何边界。
   • 由于 KS 集合对应于具有完美量子策略的双部非局域游戏（BPQS），该结果有助于设计输入基数最小的实验场景，推动量子实验的可行性。

2. 算法与计算方法的革新：

   • 解决了组合数学中“大规模同构消除”的长期瓶颈。
   • 证明了将专用工具（NAUTY）与通用求解器（SAT）结合，并通过 RCL 解决遗传性问题的有效性。
   • 该方法论可推广到其他需要无同构生成复杂组合结构的领域（如化学分子生成、网络设计等）。

3. 可验证性标准：

   • 通过扩展 DRAT 格式和独立验证器，为大规模穷举搜索提供了新的可验证性标准，消除了对求解器内部逻辑的不信任，确保了科学结论的严谨性。

总结：该论文通过创新的 SAT+NAUTY 框架和 RCL 技术，成功攻克了三维 KS 集合穷举搜索中的计算瓶颈，不仅解决了具体的物理问题（确认 Schütte 集合的唯一性），也为处理大规模组合搜索问题提供了通用的方法论范式。