Download PDFOpen PDF in browserCombining CDCL, Gauss-Jordan Elimination, and Proof GenerationEasyChair Preprint 849712 pages•Date: July 19, 2022AbstractTraditional 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. Keyphrases: Binary Decision Diagrams, Boolean satisfiability, Gauss-Jordan Elimination, clausal proofs
|