Download PDFOpen PDF in browser

Combining CDCL, Gauss-Jordan Elimination, and Proof Generation

EasyChair Preprint no. 8497

12 pagesDate: July 19, 2022


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.

Keyphrases: Binary Decision Diagrams, Boolean satisfiability, clausal proofs, Gauss-Jordan Elimination

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Mate Soos and Randal Bryant},
  title = {Combining CDCL, Gauss-Jordan Elimination, and Proof Generation},
  howpublished = {EasyChair Preprint no. 8497},

  year = {EasyChair, 2022}}
Download PDFOpen PDF in browser