M05
离散环面上的三点不共线问题：SAT/整数规划扩表与首批合数 gcd 情形的判定
1 · 研究问题
离散环面 Zm×Zn 上两两不三点共线的最大点数 τ(m,n)，在已发表计算表（2 ≤ m ≤ 7）之外的下一批值（m = 8,9,10）是多少？gcd(m,n) 为合数的最小开放情形能否判定是否达到已知上界 2·gcd(m,n)？
2 · 研究背景与空白
平面网格的 no-three-in-line 问题是经典组合几何难题；环面版本由 Misiak 等系统研究（arXiv:1203.6604）：上界 τ ≤ 2·gcd(m,n)；gcd 为素数时精确值已定（如 T(Zp×Zp²)=2p，T(Zp×Zpq)=p+1，arXiv:1406.6713）；用 Gröbner 基已算出 2 ≤ m ≤ 7、2 ≤ n ≤ 19 的全表；固定 m 时 τ 关于 n 的周期性已证（Discrete Math 2019），但周期值一般未知。
空白在 m ≥ 8 的表、合数 gcd 的精确值与周期的具体数值均开放，且原文用的 Gröbner 方法可被更高效的 SAT/ILP 编码替代。适合学生：有 ~100 个已发表值当校验集，每个新值自带证书（构型 + UNSAT/对偶界），"达到上界"与"严格小于"都是结论。
历届对照：2021 年铜奖《On Higher Dimensional Orchard Visibility Problem》与 2024 年优胜《Coloring Problems on the Triangular Lattice》分别是可见性与染色问题，均非环面共线极值。
3 · 可检验假设
- H1：SAT/ILP 编码可把表扩到 m ≤ 10、n ≤ 30，并对 ≥ 3 个合数 gcd 情形（如 gcd = 4, 6, 8, 9）给出精确判定。
- H2：新数据支持固定 z = 8, 9 的周期猜测（周期值在 ≥ 2 个完整周期内自洽），并可对其中一个用提升（lifting）论证给出证明。
4 · 量化验收标准
- 方法学校验（硬门槛）：自建"环面直线/共线三元组枚举器 + 求解器"复算已发表 2 ≤ m ≤ 7、2 ≤ n ≤ 19 全表约 100 项，逐项吻合；不吻合则后续无效（环绕直线枚举是本课题最大正确性风险，必须由该表把关）。
- 新值 ≥ 30 个；每个附极值构型证书，上界附求解器 UNSAT 记录或 ILP 对偶界。
- SAT 与 ILP 两种独立编码在 ≥ 15 个实例上同值（交叉校验）。
- 周期猜测须在 ≥ 2 个完整周期的数据内一致才可写入结论。
- 实例生成器与求解脚本开源。
5 · 数据与工具
| 用途 | 来源 / 工具 |
|---|---|
| 共线三元组枚举 | Python 自写（环面直线 = 循环子群陪集；需自行实现并用已知表校验） |
| SAT 求解 | python-sat（pysat，内置 CaDiCaL/Glucose；基数约束用内置 encodings）；mn ≤ 300 单实例分钟至小时级，UNSAT 最贵；mn > 600 超出范围 |
| ILP 交叉验证 | pulp + CBC（免费内置） |
| 已发表表 | Misiak 等论文表格——仅校验用，不计入贡献 |
| 对称性剪枝 | 环面自同构群 GL 型作用，自写轨道固定；必要时 GAP 复核 |
6 · 方法路径
- 写环面共线枚举器，对 m ≤ 7 已知表完成 100 项校验。
- 核实 pysat 基数约束编码在 mn ≈ 200 的实际表现（能力核实点）。
- 逐列扩表 m = 8 → 9 → 10，存构型与 UNSAT 证书。
- 专项攻合数 gcd 实例，加对称破缺约束提速。
- 对新数据做周期观察，选一个 z 尝试提升论证证明。
- ILP 独立复核抽样实例；分析极值构型的子群结构。
7 · 新颖性边界
问题、上界 2·gcd、素数 gcd 精确值、周期性定理均已发表（点名见第 2 块），本项目不重复声称；已发表的 m ≤ 7 表只作校验集。本项目贡献（主结论）：m = 8–10 新表 + 首批合数 gcd 情形判定 + 周期的具体数值证据（及至多一个证明实例）。价值：直接回应原作者留下的开放数据区；每个值带可机检证书，正负结论（达到/未达上界）等价有效。
8 · 决策门槛（go / no-go）
- 第 4 周末：100 项校验全过。未过则枚举器有环绕 bug，禁止扩表。
- 第 10 周末：若 m = 8 列单实例 UNSAT > 48 h → 降级一：收缩 n 范围（n ≤ 19 与原表对齐）并强制对称破缺；若仍不行，转 3 维小环面 Z2×Zn×Zk 或三角格环面小表（管线复用，扩表主结论不变，对象换为检索确认的空白格）。
- 第 24 周末：若提升证明不动 → 降级二：周期部分只报数据驱动猜想 + 两周期一致性检验；扩表与合数 gcd 判定仍撑起主结论。
- 已知困难即研究内容：UNSAT 侧的计算代价本身按实例规模报告，形成"该问题计算难度谱"的附属数据。