Traditional Boolean satisfiability (SAT) solvers based on the conflict-driven clause-learning (CDCL) framework fare poorly on formulas involving large numbers of parity constraints. The CryptoMiniSat solver augments CDCL with Gauss-Jordan elimination to greatly improve performance on these formulas. Integrating the TBUDDY proof-generating BDD library into CryptoMiniSat enables it to generate unsatisfiability proofs when using Gauss-Jordan elimination. These proofs are compatible with standard, clausal proof frameworks.

翻译：基于冲突驱动子句学习（CDCL）框架的传统布尔可满足性（SAT）求解器在处理包含大量奇偶约束的公式时表现不佳。CryptoMiniSat求解器通过引入高斯-若尔当消元法增强CDCL，显著提升了这类公式的处理性能。将TBUDDY证明生成BDD库集成到CryptoMiniSat中，使其能够在采用高斯-若尔当消元法时生成不可满足性证明。这些证明与标准的子句证明框架兼容。