Proof Generation for CDCL Solvers Using Gauss-Jordan Elimination
Reviewed by Pith T0 review T1 audit T2 compute T3 formal T4 kernel pith:HBCUH7IVrecord.jsonopen to challenge →
classification
cs.LO
keywords
cdcleliminationgauss-jordancryptominisatformulasproofproofssolvers
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.