Boolean Satisfiability via Imitation Learning¶

会议: ICLR2026
arXiv: 2509.25411
代码: https://github.com/zewei-Zhang/ImitSAT
领域: model_compression
关键词: SAT, 模仿学习, CDCL, 分支策略, 自回归, Transformer

一句话总结¶

提出 ImitSAT，首个基于模仿学习的 CDCL 求解器分支策略：通过将求解器运行压缩为无冲突的 KeyTrace 专家序列，将分支决策建模为前缀条件的自回归预测任务，以少量查询预算显著减少传播次数和求解时间，并在结构化 SAT 问题上展现良好泛化能力。

领域现状：布尔可满足性问题 (SAT) 是理论 CS 和 AI 的基石。现代求解器以 CDCL 框架为主，其中分支（branching）决策决定搜索轨迹，而单元传播 (unit propagation) 占运行时间的 80%-90%。
现有痛点：
经典分支启发式（如 VSIDS）是手动设计的，适应性有限
SATformer 仅在初始化时调整变量活跃度，搜索开始后无法影响分支
Graph-Q-SAT 使用强化学习在线代理，但 RL 需要大量探索、奖励稀疏不稳定，且仅基于当前状态快照，不利用完整历史
核心洞察：传播占 CDCL 运行时间约 88.9%（MiniSAT 实测），因此减少传播次数是加速求解的主要路径。高质量的分支决策能直接减少传播。
切入角度：用模仿学习替代强化学习——从专家轨迹中直接学习，获得密集的决策级监督信号，避免探索开销。

如何从 CDCL 求解器的运行轨迹中提取高质量的专家信号，并训练一个可即插即用的分支策略来减少传播次数？

ImitSAT 由两个核心组件构成：(1) KeyTrace 构建——将完整求解器运行压缩为仅保留存活决策的紧凑序列；(2) 自回归模仿学习器——基于前缀条件预测下一个分支决策。

KeyTrace 专家轨迹提取:
做什么：从 CDCL 完整运行轨迹 \(\mathcal{T}_t\) 中提取仅包含存活决策和传播的紧凑序列 \(\mathcal{K}_t\)
核心思路：从左到右扫描轨迹，维护工作序列 \(\mathcal{K}\)。遇到决策/传播事件直接追加；遇到回溯事件，用 \(\text{trim}_{\leq h}\) 移除所有高于回溯层级的后缀事件，再追加新决策。重启视为裁剪到层级0
关键效果：重放 KeyTrace 几乎无冲突——仅需原始 MiniSAT 运行 0.2% 的冲突、19.6% 的决策、4.3% 的传播
序列化与自回归学习器:
做什么：将 CNF 公式和 KeyTrace 前缀序列化为统一输入，训练自回归模型预测下一个签名变量
输入格式：[CNF] || F_DIMACS || [SEP] || enc(K_t) || [D]，其中 [D] 是决策探针标记
训练目标：行为克隆，最小化专家决策的负对数似然（即交叉熵）
架构：Perceiver AR（Hawthorne et al., 2022），输出潜在数组长度为1，每次查询复杂度 \(O(N)\) 而非 \(O(N^2)\)。16头注意力、12个 Transformer 块
CDCL 在线集成:
做什么：在每个决策点以小预算查询学习器，不确定时回退到 VSIDS
核心策略：前置查询调度（front-loaded）——早期决策对搜索影响最大，因此在求解初期集中使用查询预算
完备性保证：所有其他 CDCL 组件（传播、冲突分析、子句学习）不变

方法	5-15	16-30	31-60	61-100	50	100
Graph-Q-SAT (3calls)	1.00	0.94	0.89	1.15	0.71	0.85
SATformer	1.00	0.89	0.84	0.78	0.88	0.81
ImitSAT (3calls)	0.75	0.83	0.75	0.78	0.74	0.76

ImitSAT 在几乎所有变量范围上取得最低 MRPP，且 1% 胜率 \(W_{1\%}\) 也是最高的（3calls 下所有范围最佳）。

方法	JNH	AIM	PARITY	PHOLE	PRET
Graph-Q-SAT (5calls)	1.11	1.18	0.56	0.82	0.92
SATformer	1.36	1.01	0.73	1.00	1.00
ImitSAT (5calls)	0.85	0.81	0.30	0.82	0.42

仅在随机 3-SAT 上训练，无需微调即可泛化到结构化问题，在 PARITY 和 PRET 上优势尤为明显。

vs SATformer：SATformer 仅在初始化时影响 VSIDS 分数，搜索中不再干预；ImitSAT 在搜索过程中直接指导分支，更直接
vs Graph-Q-SAT：GQSAT 用 RL + 当前状态快照，奖励稀疏且不利用历史；ImitSAT 用 IL + 完整前缀历史，训练更稳定
vs MIP branch-and-bound 的 IL 方法：MIP 的 B&B 是单调树搜索；SAT 的 CDCL 有非单调搜索、重启和子句学习，动态更复杂。ImitSAT 训练全序列的自回归策略而非局部排序模型