M22
无限方格与六角格的 S-填装染色：周期构造与 SAT 不可染证明
来源说明：本则出自独立撰写的第二批方案。它与前 20 则同样遵循八块结构与硬门槛要求，但撰写时未做英文文献检索，新颖性边界依据的是历届获奖图谱与既有知识，而非当轮查新。因此其「需核实」条目更多，启动前须自行补一轮英文检索。
1 · 研究问题
对若干处于已知可染/不可染边界上的距离序列 S（如 (1,1,2,2,3,3,…) 的截断变体），无限方格图与六角格图是否存在 S-填装染色（S-packing coloring）？每个具体 S 的答案能否用"周期构造"（可染）或"有限子图 SAT 不可满足"（不可染）二者之一严格判定？
2 · 研究背景与空白
S-填装染色是填装染色（packing coloring）的推广：给定不减正整数序列 S = (s₁, s₂, …)，把顶点分成类 V₁, V₂, …，要求 Vᵢ 内任两点距离 > sᵢ。填装色数刻画"频率越高的颜色须隔得越远"的资源分配，在无限格上是近年活跃的组合问题。关键事实：周期染色一经给出即构成可染性的严格证明；有限子图上的 SAT 不可满足即构成无限格不可染的严格证明——两个方向都是定理而非数值证据，这是本题对纯 CPU 学生特别友好的原因。
已有工作：无限方格的填装色数 χρ = 15，由 Subercaseaux 与 Heule 用 SAT 求解器于 2023 年确定（上界周期构造 + 下界大规模 SAT，下界计算用了大量 CPU 时；早期文献曾把界压到 13 ≤ χρ ≤ 15）；六角格的填装色数为 7（需核实：搜索关键词 packing chromatic number hexagonal lattice 7）；三角格已知不存在有限填装染色（需核实：搜索关键词 packing chromatic number triangular lattice infinite）。S-填装染色在格与次立方图上有系列结果（需核实：搜索关键词 Gastineau Togni S-packing coloring lattice open cases），仍留有大量具体 S 的开放情形。
空白在：可染/不可染边界附近的具体 S 序列仍成批未判定，而单个 S 的判定恰好是一年期学生课题的合适颗粒度（每个方向都有严格证明的出口，且开放清单公开可查）。
3 · 可检验假设
- H1：所选 3 个开放序列 S 中至少 1 个可在六角格上用周期不超过 30×30 的周期染色证明可染。
- H2：至少 1 个所选 S 在方格上不可染，且不可染性可用直径 ≤ 40 的有限补丁 SAT 不可满足证明（笔记本可在 10⁶ 秒内跑完）。
4 · 量化验收标准
- 方法学校验（硬门槛）：自建 SAT 编码与周期验证器先复现两项已知结果——(a) 机器验证六角格 χρ = 7 的已发表周期构造合法；(b) 复现方格早期文献的一个下界补丁（如证明某小补丁不可 12-染色；具体补丁规模第 3 周从文献核实）。复现失败则编码有误，后续全部无效。
- 判定交付：至少 2 个此前开放的 S 序列获得严格判定（构造或不可染证明各算一个）。
- SAT 证明可信度：不可染方向输出 DRAT 证书并用独立工具（drat-trim）校验通过。
- 周期构造可信度：可染方向的周期染色用独立验证脚本逐对顶点检查距离约束，零违例。
- 全部编码器、构造与证书开源，一键复跑。
5 · 数据与工具
| 用途 | 来源 / 工具 |
|---|---|
| SAT 求解 | Kissat / CaDiCaL（GitHub 开源，纯 CPU）；PySAT 做编码 |
| 证书校验 | drat-trim（GitHub 开源），仅用于校验，不计入贡献 |
| 开放情形清单 | 文献综述自建表：第 3 周从 S-packing 系列论文整理（需核实最新版，搜索关键词 S-packing coloring square grid open） |
| 周期构造搜索 | 自写模拟退火/精确回溯 Python 脚本 |
| 算力量级 | 单补丁 SAT 从分钟到数天不等；选题时按"笔记本 7 天内单实例"为上限筛选目标 S |
6 · 方法路径
- 实现格图补丁生成器与 S-填装染色 SAT 编码，完成第 4 块第 1 条两项复现。
- 文献窗口：整理方格/六角格 S-填装染色的已判定与开放清单（这是关键的能力边界核实步）。
- 按"预估难度递增"排序开放 S，选 3 个目标；每个先跑小补丁 SAT 探边界。
- 可染方向：在环面（周期边界）上搜索周期染色，找到后转为无限格合法性验证。
- 不可染方向：逐步扩大补丁至 UNSAT，输出并校验 DRAT 证书。
- 独立交叉校验：换一种编码（顺序编码 vs 直接编码）复算全部主结果。
- 写明每个结论的证明形态（构造定理 / 机器证明），并讨论对相邻 S 的推论。
7 · 新颖性边界
- 本课题不声称改进方格 χρ = 15（已由 Subercaseaux–Heule 2023 确定，其下界计算远超笔记本算力），不声称提出新的 SAT 求解技术。
- 已有工作：方格 χρ = 15（SAT，2023）；六角格与三角格的填装色数已定；S-填装染色已有系列论文覆盖部分序列（第 3 周核实精确到每个 S）。丘奖相邻获奖论文：2024 优胜奖《Coloring Problems on the Triangular Lattice》（三角格染色）——本题差异：染色模型不同（S-填装 vs 该文所研究的染色）、目标格不同、且交付形态是"逐 S 的严格判定"。
- 本项目贡献（主结论）：若干开放 S 的首个严格判定，及其 DRAT 证书 / 周期构造。
- 价值：把边界向前推进可检验的一格；每个判定无论正反都是终局结论，公示期可被任何人机器复核——这在查重公示制度下是加分项。
8 · 决策门槛（go / no-go）
- 第 3 周末：完成开放清单核实。若发现目标 S 均已被 2024–2026 新文献判定 → 换清单上更靠边界的 S，框架不变。
- 第 6 周末：完成硬门槛两项复现，未过则停下修编码。
- 第 16 周末：若 3 个目标 S 全部"小补丁 SAT 可满足但找不到周期构造"（卡在中间地带），降级路径 A：改交付"可染性下界地图"——对每个 S 报告最大可染补丁半径及增长趋势（保留同一编码框架，结论形态改为定量边界）；降级路径 B：换目标格（三角格/国王格）上的同型问题，编码器复用。
- 已知困难：SAT 运行时不可预估——这本身写成研究内容（报告可满足/不可满足实例的求解时间标度）。
- 预算裁剪顺序：3 个目标 S 砍到 2 个 → 主结论（逐 S 严格判定）不变。