过程思考
长文研究笔记，记录在做研究过程中遇到的现象、错误估计、以及对引理或方法假设的修正。
本栏不是论文摘要的对外版本。它收集的是研究过程中需要长篇展开才能讲清的具体问题：某个观察现象的机制解释、某个充分条件为何在边界情形下失效、某次实验异常的来源诊断。 按时间倒序排列。
-
Dual-Bound Search 中 LB 数值收紧与 #opt 的脱耦
在 ECAI 2025 基线 Dual-Deep / Dual-Fast 上插入 Ant-Q 后，relative gap 普遍下降 23.7%–31.2% (Deep)，但 #opt 与 #min 几乎不动。这一现象不是 bug，而来自 Dual-Bound Search 框架中 LB 与 UB 之间唯一的耦合通道：硬证明规则。
-
在结构规则的 MWDS 实例上 Ant-Q 探索带来的负迁移
Ant-Q 在大多数 MWDS 实例上能改善贪心 LB 排序的质量，但在 unit disk graph 一类几何规则的实例上，引入探索反而扰动了贪心已经接近最优的序，导致 #opt 与 gap 的双重退化。本文形式化讨论这一负迁移的来源，并给出 phase-aware 关闭策略的设计。
-
DiverseSAT 作为 source problem：从 BMC 与冗余路径设计的两个归约
Diverse SAT 不是 enumeration 的另一种形式，而是若干下游应用的统一上游问题。本文从 bounded model checking 与冗余 s-t 路径设计两个例子，说明把它表述为 'k 个最大化差异的满足解' 而非 'k 个 SAT 解' 的必要性。
-
PairEF-auto 的 LP 公式拒绝一个已知公平的 allocation：Lemma 2 在 partial-access 下的过度收紧
在多资源公平分配的 meta-type 设定下，由 Lemma 2 推出的线性 EF 充分条件，会拒绝一个 DRF-MT 自身产生的 envy-free 分配。本文形式化地说明这一现象，并讨论替代的 cutting-plane 方案。
-
BIN encoding 中负数变量与 partial-product 的一个被忽略的细节
把整数变量按二进制位编入 SAT 时，partial-product 形式的乘法在变量取值有负下界时不能直接使用。本文说明这一问题在 QPLIB 一类 instance 上的具体表现，并给出基于 Booth recoding 的修正。