Proof Generation for CDCL Solvers Using Gauss-Jordan Elimination
Logic in Computer Science
2023-04-11 v1
Abstract
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.
Keywords
Cite
@article{arxiv.2304.04292,
title = {Proof Generation for CDCL Solvers Using Gauss-Jordan Elimination},
author = {Mate Soos and Randal E. Bryant},
journal= {arXiv preprint arXiv:2304.04292},
year = {2023}
}
Comments
Presented at 2022 Workshop on the Pragmatics of SAT