SC26 的 SAT 赛道里LymphoSAT 靠的是“领域专用超专业化”这条路赢下来的。这句话如果只看结果很容易被理解成“某个求解器调参调得好”但真实含义要深得多。Boolean SAT 问题本身是 NP-complete 的通用 CDCL 求解器已经非常强强到可以解出几百万变量级别的工业实例。可它强在“对大多数输入都不差”而不是针对某个具体问题域做到极致。Domain-specific hyperspecialization 的思路是放弃一部分通用性把目标领域里反复出现的结构特征全部吃进求解流程从而在特定赛道里拿到比通用求解器更稳定的成绩。这篇文章想拆的就是这条路从设计到验证再到落地的完整过程。如果你只是在项目里偶尔用用 SAT可以只看第 5 节如果你打算做竞赛级求解器或者要为一个固定问题族长期维护一套求解方案前 4 节会更值得看。1. SC26 的 SAT 赛道到底在比什么1.1 一个赛道不是一个算法题SC26 这个名字如果按 SAT 类竞赛的习惯来理解指的是某一年的 SAT 求解器赛事。它通常不是只给一个公式让你解而是准备一批 CNF 格式的布尔公式规定单实例时间上限、总时间预算、内存上限和输出格式然后比较所有参赛求解器在这批实例上的表现。关键点在这里这种竞赛不是一个“谁能在 10 秒内解出最难那道题”的比赛而是一个“谁能在规定时间内稳定地解出更多实例、并且平均耗时更少”的比赛。单个实例可能靠运气整批实例只能靠系统化设计。1.2 赛道如何计分最常见的计分方式是 solved instances 和 PAR-2solved instances在时限内给出正确结果SAT 给真值赋值UNSAT 给无关性证明的实例数量。PAR-2把每个实例的耗时放进一个平均值里未解出的实例按 2 倍时限算罚时。PAR-2 越低说明求解器的整体表现越稳定。指标计算方式关注原因solved时限内正确解出的实例数排名最直接的依据PAR-2平均解出耗时未解出按 2×timeout反映整体稳定性不同时间窗口解出比例10s / 60s / 300s 内解出数量判断是否有普遍的快速求解能力这一点直接影响设计目标如果你的求解器在某个问题域里能稳定秒解 80% 的实例但剩下 20% 全部超时你的 PAR-2 可能比不过一个“每个实例都多花点时间但全部解出”的求解器。所以赛道制胜的核心不是“灵光一闪”而是“对整批输入都有一套可预期的处理策略”。1.3 为什么会出现“领域专用赛道”不同来源的 SAT 实例差异极大。有界模型检验生成的实例有明显的时间帧结构电路等价性验证的实例保持门级连接关系调度和规划问题里有大量基数约束密码学相关的实例又会包含许多 XOR 约束。通用求解器必须兼顾这些差异因此很多结构特征它无法真正利用。领域专用赛道就是给“针对某一类问题做过专门设计”的求解器一个舞台这也是 LymphoSAT 用 hyperspecialization 赢下 SC26 SAT 赛道的大背景。2. 通用 CDCL 求解器很强但它的强是针对“平均情况”2.1 CDCL 的核心机制现代布尔求解器基本都建立在 CDCLConflict-Driven Clause Learning冲突驱动子句学习之上。核心机制可以压缩成四块单位传播每当一个变量被赋值立即推导出哪些其他子句变成单子句并强制赋值。冲突分析发现冲突以后不直接回溯而是分析冲突原因并学出一条新子句。分支启发式决定下一个分支变量选谁常用 VSIDS 或其变体。重启和遗忘定期清空当前决策栈丢弃启发式价值低的子句避免搜索路径僵化。这套机制能在工业实例上工作得很好是因为它把“搜索过程本身”变成可以学习的结构。但注意它学的是“这次搜索里哪些变量和子句重要”而不是“这个领域里哪些结构值得优先处理”。2.2 通用求解器的三个盲区第一编码信息。CNF 能表达任何 SAT 问题但同样的逻辑关系用不同编码写出来求解难度可能相差几个数量级。通用求解器不知道原始问题的语义只能看见子句列表。第二结构化预处理。某些领域里存在稳定的结构关系例如电路中的门级等价、时间帧之间的变量关联。通用求解器虽然也会做变量消除、等价替换、子句消除但这些预处理是面向一般 CNF 的不是针对某个领域优化的。第三启发式和参数边界。VSIDS 的衰减率、重启策略、LBD 截断值这些参数的最佳区间随实例族变化很大。通用求解器只能选一组在多个领域上都不太差的默认值。所以hyperspecialization 的本质不是“不用 CDCL”而是把 CDCL 这条流水线里的每一层都替换成或叠加进针对目标领域的专用逻辑。3. LymphoSAT 这条路线领域专用超专业化是怎么落地的3.1 把目标领域拆成可测量的结构特征我不清楚 LymphoSAT 内部具体用了哪些模块但按照这类路线的通用做法第一件事不是写代码而是对目标实例集做一次“数据画像”。一般我会做这样几项统计变量数和子句数分布、单子句/二元子句/三元子句占比变量出现次数分布有没有明显的幂律特征子句平均长度和长度分布SAT/UNSAT 的比例固定参数下的基线求解耗时分布如果能拿到还可以分析 UNSAT 核心、变量社区结构、以及可等价化简的变量对。这些数字决定了该往哪个方向做专用化。比如子句长度普遍偏短可以强化二元子句推理如果有大量 XOR 约束正规 CDCL 可能还需要叠加线性代数推理如果问题是天然不满足的可能需要优先做更激进的化简而不是更快地搜索。3.2 把领域知识放进编码、预处理和启发式竞赛级专用求解器一般会在三个层面做文章。编码层。如果需要自己生成 CNF可以考虑用更贴近原始问题语义的编码方式比如为基数约束加辅助变量、把等价关系用链式编码减少中间变量。如果求解对象是别人给的固定 CNF这一步通常做不了但可以识别里面的子结构例如检测 XOR 子句、基数子句再决定是否启用特殊传播器。预处理层。领域知识经常在这里增值最大。对电路类实例门级等价和扇出结构可以用来做变量分组对有界模型检验实例时间帧之间的对应关系可以做跨帧化简对包含大量对称性的问题可以加入对称破缺。通用求解器也做这些事的一部分但专用求解器可以把它们做得更激进因为知道目标实例不会因为激进化简而崩坏。启发式层。分支变量选择、相位保存、重启策略、子句删除阈值这些都是可以按领域定制的。常见的做法包括用统计到的变量出现频率初始化 VSIDS 活动度在搜索早期偏向某个相位因为目标领域里有明显的极性偏向调整 LBD 截断值和子句保留比例控制内存消耗和重启节奏。这里很容易犯一个错误一上来就调分支启发式。我的建议是先确认编码和预处理已经把你对领域的理解吃进去了再到启发式层做增量调整。因为启发式的改进通常只有几个百分点到十几个百分点而预处理不当可能改变整个问题的求解难度。3.3 让求解器符合赛道需要的“可验证输出”竞赛不是把结果打印出来就行。SAT 实例要能校验你给出的变量赋值UNSAT 实例通常要能输出 DRAT 格式的步骤由官方校验器检查。很多求解器在测试阶段都栽在“能快速得到答案但答案无法通过校验”上。所以专用求解器在落地前必须把两件事写成自动化对 SAT 结果保存模型用独立解析器重新判定模型确实满足所有子句对 UNSAT 结果开启 DRAT 或 FRAT 等证明输出用竞争类型校验器跑一遍。我一般会把这两步放进 CI 流程而不是每次手工验证。这样每次改启发式、改预处理都能立刻知道是不是引入了验证层面的 bug。4. 从单实例到完整参赛验证一套专用求解器的流程4.1 基准划分不能只看“公不公平”竞赛提供的基准池往往就是训练素材。如果直接把所有基准都拿来调参最后得分可能很高但那是过拟合。更稳妥的做法是把基准池按实例来源或难度分层一部分用于开发一部分用于每轮消融验证留一部分作为“最后只能跑一次的盲测集”。盲测集的划分要尽量模拟比赛环境包括同样的超时设置和机器环境。4.2 用哪些指标衡量一个改动我自己的习惯是同时看 5 个数字总解出数量PAR-2SAT 实例和 UNSAT 实例分别的解出率不同时间窗口内10 秒、60 秒、300 秒的解出比例最大单体耗时是否接近超时线。如果某个改动让总解出数上升但 SAT 实例解出率下降这种变化在竞赛里通常不划算因为赛道排名往往对整体稳定性更敏感。如果改动降低 PAR-2 但导致内存峰值上升也要小心因为竞赛机器有内存上限。4.3 消融实验是专用求解器的“体检报告”领域专用求解器最大的风险是你以为某个模块有用其实它只是没造成伤害。所以每加一个专用模块都要做一次消融实验关掉它在同一批实例上重跑比较指标变化。做得规范一点可以写一个配置矩阵脚本把每个模块的开关组合都跑一遍。我见过不少团队把十几个启发式堆在一起最后发现其中两三个是负贡献只是被其他模块掩盖了。这类问题如果在参赛前没发现比赛时会在某个实例族上突然爆发。4.4 多次随机种子和稳定性检查CDCL 求解器带有随机性分支选择、重启、相位都可能受到随机种子影响。同一个求解器在同一个实例上用不同种子耗时可能差 3 倍。因此在评估阶段最好每个实例用多个种子跑观察耗时分布而不是只看单次结果。不要只用一次运行的结果判断“这个模块有效”。在我自己的测试里某次改动单种子跑快了 40%换 5 个种子之后优势只剩 8%其中一个种子上反而更慢。竞赛里常见的做法是用 10 到 20 个种子跑关键基准以分布和汇总指标为准。5. 竞赛之外这五条经验能直接迁移到实际项目5.1 不是所有问题都要从零写求解器如果你的问题是几十个通用 SAT 实例直接用开源 CDCL 求解器最合适。领域专用化只有在“同一个问题域会反复生成大量实例”时才值得投入。比如你有一个约束建模前端每次生成的 CNF 结构同源那么专用求解器的收益会随实例数量放大。5.2 先做数据画像再谈启发式真实项目里最常见的开局是“先找个求解器跑一下跑慢了再调”。正确的顺序应该是先把典型实例收集齐统计结构特征、耗时分布和失败模式。没有画像后面所有优化都是盲调。5.3 编码和预处理常常比搜索启发式更值钱这一点怎么强调都不过分。同样的逻辑约束换成不同编码求解时间可能差 10 倍甚至更多。对固定建模前端花时间改进编码或在预处理阶段做局部化简往往比在分支启发式上磨一个月更划算。搜索启发式优化是在“问题已经被良好建模”的前提下才有高边际收益。5.4 时间预算和不确定性要提前设计竞赛有时间上限实际项目里也有。交互式工具可能要求 1 秒内返回离线批处理也许允许跑 1 小时。不同的时间预算要求完全不同的资源配置短时间场景下参数和预处理要更保守长时间场景下可以考虑保存求解中间状态、断点续算。这些要在架构层面预留而不是上线后再补。5.5 建立可重复的验证基准很多项目上线后改崩了都不知道就是缺一个固定基准集加自动回归。建议至少维护三类实例代表线上真实分布的实例、代表最难边界的实例、代表历史回归问题的实例。每次改动跑一遍超时规则和校验方式与线上保持一致。6. 容易翻车的五个地方和一套排查顺序6.1 五个常见误判第一把“解出数量多”等同于“解出难度高”。有的专用求解器是靠快速解决大量简单实例拿分的真正难的实例还是解不动。竞赛排名看的是整体但如果目标是解决硬问题就应该只看硬实例上的表现。第二在测试基准上调参。这会让结果虚高也让你无法判断新参数是否真的泛化。第三跳过 UNSAT 证明校验。很多专用化改造会影响子句删除和重写逻辑一旦子句删除出错UNSAT 结果可能无效。没有校验你的“胜利”可能是靠错误输出换来的。第四单种子评估。CDCL 的随机性很强单次耗时不能代表真实性能。第五过度调整重启策略。重启策略和分支启发式、子句删除策略强耦合单独调一个变量很容易出现“这组参数在 A 实例族上变好、在 B 实例族上变差”的情况。6.2 当你发现结果变差时按这个顺序排查我会先按下面的顺序找原因而不是一上来就改参数先看现象是超时变多还是输出校验失败还是内存被挤爆。再看输入同样的实例在不同机器或不同编码下是否有差异文件是否完整是否有隐藏的空行、注释、重复子句。再看环境和依赖编译器版本、优化开关、运行时库、随机种子是否一致多线程求解时线程数设置是否合理。再看预处理输出确认预处理后的 CNF 是否和原公式等价有没有因为激进化简引入了错误。再看参数对刚改动过的配置先做 diff确认是不是某个参数组合把时间预算耗在了前置环节。最后回到基线对比用一个已知稳定的开源求解器或上一个版本在同样实例上跑一遍判断问题是出在算法还是出在配置。这套顺序的好处是能快速排除“不是求解器的问题”这类情况。实际排错中我遇到最多的并不是算法本身退步而是机器内存不足、子句删除开关没生效、或者 UNSAT 证明输出被缓存文件覆盖。6.3 给想走这条路的人一个保守建议如果你想复现 LymphoSAT 这种“领域专用超专业化”的路线不要一开始就追求从头写一个 CDCL 框架。先用现成求解器作为基线把目标数据集统计分析做到位再考虑在预处理层和启发式层做增量改造。等你的消融实验证明某个专用模块对目标实例族有稳定收益再逐步加深专用化。反而是这种“先跑通、再画像、再专用、再验证”的顺序更容易在有限时间内得到一个真正能赢的求解器。