将 CDCL 扩展至命题方程的析取形式

由于 CDCL 产生的是 Resolution 证明系统中的证明，对于 Resolution 难以解决的问题，CDCL 也同样难以解决。某些情况下，使用更强的证明系统（如 $\text{Res}(\oplus)$）可找到指数级更短的证明。该系统是 Resolution 对 XNF 公式的推广，其约束为命题方程的析取（“线性从句”），例如 $(x \oplus y) \lor \lnot (y \oplus z)$。虽然部分现代求解器（如 CryptoMiniSAT）在布尔从句上独立处理命题方程，但针对更一般的线性从句的推理仍鲜有探索。我们提出了 $\text{CDCL}(\oplus)$，即针对 XNF 公式的 CDCL 推广，证明了其与 $\text{Res}(\oplus)$ 之间的双向等价性：$\text{CDCL}(\oplus)$ 不仅能产生 $\text{Res}(\oplus)$ 证明，还能在非确定性决策和重启的条件下多项式时间模拟 $\text{Res}(\oplus)$，这反映了 CDCL 与 Resolution 之间的经典关系。我们的关键技术工具是为 $\text{Res}(\oplus)$ 设计的新的推理规则，帮助我们将诸如 1-UIP 从句学习等基于 Resolution 的子程序进行翻译。总体而言，$\text{CDCL}(\oplus)$ 的命题推理包括：对任意命题方程的分支、单位传播中的线性代数推理，以及通过冲突分析学习线性从句。我们实现了一个概念验证性的 $\text{CDCL}(\oplus)$ 求解器，命名为 Xorcle，其中包括针对 XNF 公式的现有 CDCL 启发式方法的调整，以及我们称之为 $\text{LRUP}(\oplus)$ 的 LRUP 证明日志的扩展。在聚焦于原生 XNF 公式的精选基准测试中，Xorcle 在已有求解器（如 Kissat 和 CryptoMiniSAT）之上取得了优势。此外，在未经预处理的情况下，对用 CNF 书写的 Tseitin 公式，Xorcle 的运行时间似乎接近多项式时间缩放。