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 求解器通过添加 Gauss-Jordan 消元来大大提高这些公式的性能。将 TBUDDY 证明生成 BDD 库集成到 CryptoMiniSat 中，使其能够在使用 Gauss-Jordan 消元时生成不可满足性证明。这些证明与标准子句证明框架兼容。