技术摘要：将 CDCL 扩展至奇偶方程的析取

问题陈述

冲突驱动子句学习（CDCL）是 SAT 求解的主导方法，但其根本上受限于归结（Resolution）证明系统。那些在归结中需要指数级证明规模的问题（如 Tseitin 公式或双射鸽巢原理），被证明对 CDCL 而言是困难的。尽管一些求解器集成了更强证明系统的片段——例如使用切割平面（Cutting Planes）的伪布尔求解器，或处理奇偶方程的 CNF-XOR 求解器——但这些方法通常将奇偶推理视为独立模块，或局限于特定的范式（如 CNF-XOR）。

本工作旨在填补的具体空白是：缺乏一种能够原生处理XNF（XOR-OR-AND 范式）公式的 CDCL 风格算法。XNF 公式由线性子句的合取组成，线性子句是奇偶方程的析取（例如 $(x \oplus y) \lor \neg(y \oplus z)$）。虽然**Res(⊕)**证明系统（推广至 XNF 的归结）已知对某些问题比归结具有指数级优势，但现有求解器并未将 Res(⊕) 推理完全集成到 CDCL 循环中，也未提供理论证明表明 CDCL 风格算法可以多项式模拟 Res(⊕)。

方法论

作者提出了CDCL(⊕)，这是一种旨在直接操作 XNF 公式的 CDCL 算法推广。该方法依赖于三个核心组件：

1. Res(⊕) 的新推理规则：
   作者引入了 Res(⊕) 证明系统的新表征，用加法和基变换取代了标准的归结和弱化规则。

   • 加法： 从 $C \lor f$ 和 $D \lor g$ 推导出 $C \lor D \lor (f + g)$。
   • 基变换： 从 $C$ 推导出任意 $D$，使得 $C \equiv D$（语义等价）。
     关键在于，他们定义了一条仿射归结规则，其中方程通过“基变换”被“隔离”，从而允许通过加法进行消去。这消除了与弱化规则相关的指数级搜索空间，实现了多项式模拟。

2. 基于线性代数的单元传播：
   与基于文字赋值进行传播的经典 CDCL 不同，CDCL(⊕) 使用 $\mathbb{F}_2$ 上的线性代数执行单元传播。

   • 求解器维护一组已知的单元（方程）$U$。
   • 传播检查给定 $U$ 时，线性子句 $C$ 是否蕴含新方程 $f$ 或矛盾（$1$）。
   • 其实现方式是将子句的“线性否定”（即 falsifying 该子句的赋值子空间）相对于 $U$ 的张成空间进行约化。如果子句的否定包含在 $U$ 的张成空间加上单个方程 $f$ 之内，则推导出 $f$。

3. 通过冲突分析进行子句学习：
   本文将 1-UIP（首个唯一蕴含点）子句学习策略适配到 XNF 环境。由于蕴含图不能直接转化为线性方程，学习算法在语义上运行：

   • 它从冲突子句（矛盾的原因）开始。
   • 它迭代应用基变换以隔离导致最近决策的方程。
   • 它应用加法规则，将隔离后的子句与冲突原因相结合，从而有效地消去决策变量。
   • 该过程重复进行，直到找到断言子句（即在当前决策层级强制进行传播的子句）。

主要贡献

理论贡献

• 双向联系： 本文证明了 CDCL(⊕) 不仅产生 Res(⊕) 证明，而且在非确定性决策和重启的前提下，能够多项式模拟Res(⊕) 证明系统。这反映了经典 CDCL 与归结之间的关系。
• 新证明系统表征： 作者提供了一组新的推理规则（加法和基变换），它们在多项式上等价于 Res(⊕)，但缺乏弱化规则，因此更适合算法实现。
• 输入 Res(⊕) 等价性： 本文证明了 CDCL(⊕) 中的单元传播等价于 Res(⊕) 的一个片段，称为输入 Res(⊕)，推广了经典 CDCL 的已知结果。
• 改进的模拟因子： 模拟证明改进了经典 CDCL/归结关系的多项式因子（通过优化子句分解的吸收方式，以更简单的论证匹配了 [7] 中的结果）。

实践贡献

• Xorcle 实现： 作者提出了Xorcle，一个用于 CDCL(⊕) 的概念验证求解器。
  • 它使用位打包实现了 $\mathbb{F}_2$ 上的高效线性代数。
  • 它引入了CSIDS（子句状态独立衰减和），这是一种新的子句选择启发式方法，将 VSIDS 和 CMTF 推广到 XNF 上下文。
  • 它引入了LRUP(⊕)，这是对 LRUP 证明日志格式的扩展，以支持奇偶表达式。
• XNF 启发式方法： 本文详细说明了针对监视结构的适配（由于线性依赖，循环遍历子句而非维护复杂的监视列表）、决策过程（从子句的否定中随机分支方程）以及相位选择（优先 falsify 子句）。

实验结果

作者在以下基准测试套件上评估了 Xorcle：

• Ascon-128： 与密码学相关的 2-XNF 族。
• 随机和受限 k-XNF： 具有不同变量和方程数量的合成公式。
• Tseitin 公式： 以 CNF 编码的奇偶问题，已知对归结而言是困难的。

主要发现：

• XNF 上的性能： 在原生 XNF 基准测试中，Xorcle 优于现有求解器（Kissat、CryptoMiniSAT 和 2-Xornado）。值得注意的是，尽管使用通用 XNF 推理，它在 Ascon-128 实例上仍优于 2-Xornado（一种专用的 2-XNF 求解器）。
• Tseitin 公式上的性能： 在编码为 CNF 的 Tseitin 公式上，Xorcle 展示了近乎多项式的运行时间扩展，而基于归结的求解器众所周知需要指数时间。这是在不进行预处理、仅依赖核心 CDCL(⊕) 推理的情况下实现的。
• 决策质量： Xorcle 所需的决策次数显著少于竞争求解器，这表明基于奇偶的分支和推导机制对这些问题的类别更为有效。

意义与主张

本文声称，CDCL(⊕) 提供了首个将奇偶推理完全集成到 CDCL 范式中的严谨理论框架和实际实现。

• 理论意义： 它确立了 CDCL 的局限性并非源于算法结构，而是源于底层证明系统（归结）。通过转向 Res(⊕)，CDCL 理论上可以解决那些对标准 CDCL 呈指数级困难的问题。
• 实践意义： 结果表明，原生 XNF 求解是可行的，并且可能优于将 XNF 转换为 CNF 或 CNF-XOR。能够在几乎无需预处理的情况下以近乎多项式时间求解 Tseitin 公式，突显了奇偶推理克服 SAT 求解中已知困难障碍的潜力。
• 未来方向： 作者谦逊地指出，Xorcle 是一个概念验证。它目前缺乏若干标准 CDCL 优化（例如子句删除、高级重启、动态启发式），并且尚未将"1-UIP"或“子句最小化”等概念完全推广到语义 XNF 环境。这项工作为针对隐式需要奇偶推理的 CNF 公式的启发式方法研究打开了大门。