# Proof Generation for CDCL Solvers Using Gauss-Jordan Elimination

arXiv: https://arxiv.org/abs/2304.04292 · HTML: https://mlsanity.com/paper/2304.04292/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 9 Apr 2023.

## Built on by (most cited first, 2 of 2)

- [Formally Certified Approximate Model Counting](https://mlsanity.com/paper/2406.11414/) (2024)
- [IGMaxHS -- An Incremental MaxSAT Solver with Support for XOR Clauses](https://mlsanity.com/paper/2410.15897/) (2024)

## Abstract (arXiv)

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.