Because CDCL produces proofs in the Resolution proof system, problems provably hard for Resolution are also provably hard for CDCL. Exponentially shorter proofs can sometimes be found using stronger proof systems such as $\text{Res}(\oplus)$, a generalization of Resolution to XNF formulas, whose constraints are disjunctions of parity equations ("linear clauses") such as $(x \oplus y) \lor \lnot (y \oplus z)$. While some modern solvers like CryptoMiniSAT reason on Boolean clauses with separate parity equations, reasoning about more general linear clauses is less explored. We present $\text{CDCL}(\oplus)$, a generalization of CDCL to XNF formulas, and prove a bidirectional connection with $\text{Res}(\oplus)$: $\text{CDCL}(\oplus)$ not only produces $\text{Res}(\oplus)$ proofs, but also polynomially simulates $\text{Res}(\oplus)$ given nondeterministic decisions and restarts, mirroring the classical relationship between CDCL and Resolution. Our key technical tool is a new set of inference rules for $\text{Res}(\oplus)$ that helps us translate Resolution-based subroutines such as 1-UIP clause learning. Altogether, $\text{CDCL}(\oplus)$'s parity reasoning includes branching on arbitrary parity equations, linear-algebraic reasoning during unit propagation, and learning linear clauses through conflict analysis. We provide a proof-of-concept implementation of $\text{CDCL}(\oplus)$ called Xorcle, which includes adaptations of existing CDCL heuristics to XNF formulas and an extension of LRUP proof logging that we call $\text{LRUP}(\oplus)$. On a selected suite of benchmarks focusing on native XNF formulas, Xorcle outperforms existing solvers such as Kissat and CryptoMiniSAT. Additionally, on Tseitin formulas written in CNF, even without preprocessing, Xorcle's running time appears to scale nearly polynomially.

翻译：由于CDCL在Resolution证明系统中生成证明，因此对于Resolution而言证明困难的问题，对于CDCL也同样困难。使用更强的证明系统（例如$\text{Res}(\oplus)$）有时可以找到指数级更短的证明。$\text{Res}(\oplus)$是将Resolution推广到XNF公式的系统，其约束是奇偶方程析取（"线性子句"），例如$(x \oplus y) \lor \lnot (y \oplus z)$。虽然一些现代求解器（如CryptoMiniSAT）在布尔子句与独立奇偶方程上进行推理，但对更一般的线性子句的推理研究较少。我们提出了$\text{CDCL}(\oplus)$，这是将CDCL推广到XNF公式的框架，并证明了它与$\text{Res}(\oplus)$之间的双向联系：$\text{CDCL}(\oplus)$不仅能生成$\text{Res}(\oplus)$证明，而且在非确定性决策和重启条件下可多项式模拟$\text{Res}(\oplus)$，这对应了经典CDCL与Resolution之间的关系。我们的关键技术工具是一组$\text{Res}(\oplus)$的新推理规则，这有助于翻译基于Resolution的子例程（如1-UIP子句学习）。总体而言，$\text{CDCL}(\oplus)$的奇偶推理包括：对任意奇偶方程进行分支、在单元传播过程中进行线性代数推理、以及通过冲突分析学习线性子句。我们提供了$\text{CDCL}(\oplus)$的概念验证实现Xorcle，其中包括将现有CDCL启发式方法适配到XNF公式，以及我们称之为$\text{LRUP}(\oplus)$的LRUP证明日志记录扩展。在针对原生XNF公式的选定基准测试集中，Xorcle的性能优于Kissat和CryptoMiniSAT等现有求解器。此外，在处理以CNF形式编写的Tseitin公式时，即使未进行预处理，Xorcle的运行时间也几乎呈多项式级扩展。