基数约束 CNF 编码的求解成本敏感性：已发表编码排名在新求解器与新实例族上的独立检验

1 · 研究问题

把组合问题编码为命题可满足性（SAT）实例时，"至多一个"（at-most-one, AMO）与基数约束（cardinality constraint）的六种经典 CNF 编码（pairwise、sequential/Sinz 计数器、commander、bimander、product、totalizer）之间的求解成本排名，在换用 2020 年后的现代 CDCL（conflict-driven clause learning）求解器 CaDiCaL / Kissat 并换用一组独立的实例族后，是否仍与文献报告的排名一致？若排名发生翻转，翻转能否由编码引入的辅助变量数与子句数这两个可先验计算的量解释？

2 · 研究背景与空白

技术背景。 大量组合问题（图着色、排课、拉丁方补全、Golomb 尺、装箱）在转成 SAT 之前必须把"这组布尔变量中至多有一个为真"这类计数条件翻译成 CNF 子句。最朴素的 pairwise 编码写出全部 C(n,2) 条互斥子句，子句数是平方级但不引入辅助变量；Sinz 的顺序计数器用 O(n) 个辅助变量把子句数降到线性；commander、bimander、product 编码在两者之间取折中；totalizer 与排序网络编码则支持一般的 ≤k 约束。这里存在一个非平凡的权衡：子句数少不等于求解快，因为辅助变量会改变求解器的决策堆与子句学习行为，而单位传播（unit propagation）的强度——即某个编码能否在赋值后立刻推出更多蕴涵——往往才是决定性因素。这类课题的资源特性极其友好：SAT 求解是纯 CPU、单线程、内存需求通常在几百 MB 内的整数运算任务，笔记本与服务器的唯一差别只是能跑多少个实例，而不是能不能跑。学生只需要把时间预算换成实例数量。

已有工作到哪一步。 Nguyen 的《Empirical Study on SAT-Encodings of the At-Most-One Constraint》（SMA 2020）在三个当时主流求解器上系统比较了主要 AMO 编码；该研究在 Golomb 尺实例上用 Lingeling 求解器报告：commander 编码最快，binary 与 pairwise 编码也表现良好，而 product、bimander 与 sequential 编码表现很差。Wynn 的《A comparison of encodings for cardinality constraints in a SAT solver》（arXiv:1810.12975）比较了 Sinz 顺序计数器、Bailleux–Boufkhad 树形与 Abío 等的排序网络三类方法，结论是顺序计数器在一系列组合测试用例上最快；另有对照研究报告在成功案例中顺序计数器编码在 113 个实例上取得最优运行时、totalizer 在 92 个实例上最优。这些结论彼此并不完全一致，且所用求解器多为 Lingeling、Clasp、Riss3G 等 2010 年代中期的版本。

空白在于：现代 CDCL 求解器（CaDiCaL、Kissat，2019 年后多次夺得 SAT 竞赛冠军）引入了内联处理（inprocessing）、变量消去与子句消减等预处理，而这些技术恰恰会主动消掉编码引入的辅助变量——这意味着"哪种编码更好"的旧结论有可能已经被求解器的进步抹平或反转，但没有公开工作在新求解器上做过这项独立检验。这个空白属于最可靠的类型——换样本的独立检验（新求解器 + 新实例族）：方法完全公开、实例可自行生成、算力门槛极低、且结论正负都成立（排名稳定则说明编码选择是求解器无关的结构性因素；排名翻转则说明既有的编码选择建议已过时）。

3 · 可检验假设

• H1：在 CaDiCaL 与 Kissat 上，六种 AMO 编码之间的 PAR-2 分数（惩罚平均运行时，超时按 2 倍时限计）差异，比在 MiniSat（无内联处理的经典基线）上显著缩小——具体判据为：最优与最差编码的 PAR-2 比值，从 MiniSat 上的 ≥ 3 倍降至现代求解器上的 ≤ 1.8 倍。
• H2：若 H1 不成立（差异仍然巨大），则编码排名可由"辅助变量数 / 原变量数"这一比值单调预测：跨 4 个实例族 × 6 种编码的 24 个点上，PAR-2 排名与该比值的 Kendall τ ≥ 0.5。若两者都不成立，则说明编码优劣由实例族特性主导而无通用规律——这同样是有效结论，且直接否证了文献中"某编码普遍最好"的表述。

4 · 量化验收标准

1. 方法学校验（硬门槛）：用自建的编码生成器 + 求解流水线，在文献使用过的实例族（Golomb 尺，阶数覆盖文献报告范围）上、用文献所用的同一代求解器（MiniSat 或 Glucose，可从官方仓库编译）重现已发表的编码排名。判据：编码之间的相对排名（按中位求解时间）与文献报告完全一致，且绝对时间在同一数量级（跨硬件允许 5 倍以内偏差）。这一步不过关，说明编码生成器本身有误，后续全部结论无效。
2. 编码正确性校验（第二道硬门槛）：每种编码在 n ≤ 12 时必须通过穷举等价性检验——枚举全部 2ⁿ 个原变量赋值，验证"存在辅助变量的延拓使公式为真"当且仅当该赋值满足原约束。这是编码类课题唯一能排除"跑得快是因为编错了"的证据，必须写进正文。
3. 重尾统计口径：SAT 求解时间是重尾分布，明确写明不报均值。统计量固定为：中位数与 IQR、PAR-2 分数、仙人掌图（cactus plot，横轴已解实例数 / 纵轴累计时间）、以及每实例的成对比较（同一实例上编码 A 是否快于 B）用 Wilcoxon 符号秩检验。超时统一设为 300 秒并在正文说明该阈值对结论的敏感性（额外用 600 秒重跑最难的 20% 实例）。
4. 随机性控制：现代求解器含随机化成分，每个（实例 × 编码 × 求解器）组合用 5 个不同的固定求解器种子各跑一次，报告 5 次的中位数；同时报告种子内方差与编码间差异的量级对比——若种子方差大于编码差异，则任何编码排名都不成立，这一判断必须在正文中给出。
5. 样本量：≥ 4 个实例族（Golomb 尺、图着色、拉丁方补全、鸽巢/装箱各一），每族 ≥ 30 个规模递增实例，总实例数 ≥ 120；实例生成脚本与种子公开。
6. 双成本口径：与文献对照时报等工作量（相同实例集上的求解时间）与等墙钟时间预算（固定 1 小时总预算下各编码能解出的实例数）两种口径，两者结论不一致时必须讨论。
7. 可复现性：编码生成器、实例生成器、全部 CNF 文件的生成脚本（不必上传 CNF 本身）、原始计时 CSV、绘图脚本全部开源；一键重跑脚本；全部种子写死。

5 · 数据与工具

用途	来源 / 工具
现代 CDCL 求解器	CaDiCaL（GitHub arminbiere/cadical，C++，无外部依赖，./configure && make 即可）；Kissat（GitHub arminbiere/kissat，C，同样零依赖）。仅用于校验与对比，不计入本项目贡献
历史基线求解器	MiniSat 2.2 / Glucose（用于复现文献排名；老代码在新编译器上可能需小改，列为风险项，需核实）
编码生成	自行实现六种编码（Python，每种 30–80 行）。可用 PySAT（python-sat 包）的 pysat.card 模块做独立交叉校验——PySAT 内置 seqcounter、sortnetwrk、cardnetwrk、totalizer、mtotalizer、kmtotalizer 等编码，但 commander / bimander / product 等 AMO 变体是否全部内置需核实，未内置的必须自行实现
实例族	Golomb 尺（自行生成，规则明确）；图着色实例用 DIMACS 图着色基准（公开，mat.tepper.cmu.edu / DIMACS 官方镜像）；拉丁方补全与鸽巢实例自行生成（参数化脚本）；另可从 SAT Competition 官方基准归档中挑选组合类实例（satcompetition.org，实例文件较大，按需下载）
穷举等价性检验	自行实现（n ≤ 12 时 2ⁿ ≤ 4096，毫秒级）
统计与作图	Python + SciPy（Wilcoxon 符号秩）+ Matplotlib（仙人掌图）
算力	纯 CPU 单线程。单实例内存通常 < 500 MB；总工作量 = 120 实例 × 6 编码 × 3 求解器 × 5 种子 × ≤ 300 秒 ≈ 最坏 900 小时，必须通过"先跑小规模筛掉平凡实例、只对非平凡区间做全扫描"控制，实际目标控制在 60–100 机时（夜间批跑两周内完成）。这一算力规划本身要写进方法路径

6 · 方法路径

1. 装环境，编译 CaDiCaL / Kissat / MiniSat，用各自仓库自带的算例确认安装正确（求解结果与官方期望一致）；跑通 PySAT 并对比其内置编码与自实现编码在小 n 上的等价性。
2. 实现六种 AMO/基数编码，逐一通过 n ≤ 12 的穷举等价性检验（验收第 2 条）；此步不过不进入下一步。
3. 核实工具能力边界：PySAT 内置了哪些编码、缺哪些需自行实现；CaDiCaL/Kissat 的内联处理开关是否可关闭（这决定 H1 能否做"开/关内联处理"的受控对照——若可关闭，这是 H1 最直接的因果检验，须优先确认）。
4. 生成实例族并做难度定标：对每族先用二分搜索找到"中位求解时间落在 1–100 秒"的规模区间，只在该区间内取 30 个实例。这是控制总算力的关键步骤，判据须写死并公开（避免选择性挑实例的嫌疑）。
5. 完成方法学校验（验收第 1 条）：在 MiniSat/Glucose 上重现文献排名并归档。
6. 执行主扫描并做重尾统计分析：PAR-2、仙人掌图、成对 Wilcoxon 检验、种子方差与编码差异的量级对比；输出 H1/H2 的判定。
7. 独立交叉校验：（a）用 PySAT 内置编码复算至少两种编码的结果，验证自实现无误；（b）若第 3 步确认可关闭内联处理，在 CaDiCaL 上做"内联处理开 vs 关"的受控对照，直接检验"求解器进步抹平编码差异"这一机制假设。

7 · 新颖性边界

本课题不声称：不提出新的编码方案，不声称任何编码"最优"，不改进求解器，不给出任何新的复杂度下界（AMO 编码的 CNF 大小下界已有专门工作，见 arXiv:1704.08934，本项目不涉足）。CaDiCaL、Kissat、PySAT、DIMACS 基准均为他人工作，标注为对照基准，不计入本项目贡献。

已有工作完成了什么：Nguyen（SMA 2020）在 Lingeling 等三个求解器上给出了 AMO 编码的经验排名，包括 Golomb 尺上 commander 最优、sequential 与 product 很差这一具体结论；Wynn（arXiv:1810.12975）比较了三类基数约束编码并报告顺序计数器最快；另有工作报告顺序计数器与 totalizer 在不同实例上各占优（113 vs 92 例）。这些结论本项目引用而不重复声称。

本项目的贡献：把这些排名放到 2020 年后的求解器（CaDiCaL / Kissat）与一组独立实例族上做重现检验，并用"内联处理开/关"的受控对照给出机制解释。主结论是"既有编码选择建议在现代求解器上是否仍然有效"这一判断本身，而不是任何新编码。

为什么有价值：编码选择是每一个把组合问题交给 SAT 求解器的人都要做的决定，现行教科书与工具默认值大多沿用 2010 年代的经验结论。若排名稳定，这些建议获得一次独立支持；若被现代求解器抹平，则"编码调优"这一整类工程努力的边际收益需要重新评估。

风险提示："六种编码差异不显著"是完全可能且有价值的结果，但必须先通过第 4 条的种子方差对比证明本实验有能力分辨题设中 1.8 倍这一量级的差异；若种子方差本身就超过 1.8 倍，则必须扩大种子数或实例数，不得直接下"无差异"结论。

8 · 决策门槛（go / no-go）

• 第 4 周：编码正确性门槛。若六种编码中有任何一种无法通过 n ≤ 12 的穷举等价性检验且两周内修不好，降级路径 A：把该编码替换为 PySAT 内置的等价编码并在正文声明来源，编码集缩为 5 种自实现 + 1 种引用。主结论框架不变。
• 第 8 周：求解器可用性与内联处理开关必须核实完毕——这是需要提前确认而非边做边发现的事项。若 MiniSat/Glucose 无法在现代编译器上构建，降级路径 B：历史基线改用 CaDiCaL 的早期版本（仓库有 tag，可回退编译）或 Glucose 的社区维护分支；若都失败，则把"新旧求解器对照"这一轴替换为"内联处理开/关"对照——后者在同一份代码内完成，机制解释力反而更强，主结论框架完全保留。
• 第 14 周：难度定标必须完成，且总算力预算必须落在 100 机时以内。若定标显示某实例族在可行规模内全部秒解或全部超时，降级路径 C：替换该族（备选：装箱、幻方补全、图的支配集），实例族数量下限保持 4 个。
• 第 32 周：主扫描完成且 H1 有明确判定。若此时扫描进度不足 60%，降级路径 D：把求解器从 3 个减为 2 个（CaDiCaL + MiniSat，保留"新 vs 旧"这一核心对照），种子数从 5 减为 3，实例族保持 4 个。宁可减求解器数量，不可减实例族数量——跨族一致性是本课题反驳"某编码普遍最好"的核心证据。
• 预算裁剪顺序：求解器数量 → 种子数量 → 每族实例数（下限 20）→ （绝不裁剪）实例族数量与穷举等价性检验。
• 选择前提：适合喜欢离散数学与组合问题、能接受"主要产出是一张严谨的否证性表格而非一个新算法"的学生。本路线代码量最小、算力需求最低，是全部十条中最不容易因工程问题失败的一条，但对统计严谨性要求最高。

---