Producing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver
summary
Adapts Flatt et al.’s greedy redundant-edge algorithm into the SMT solver cvc5 and shows it produces smaller congruence explanations by keeping and weighting redundant equalities, with a level system to avoid circular proofs and fuel limits to bound cost. Evaluation on SMT‑LIB benchmarks reports about 3% reduction in final proof size, ~8% average reduction in local explanations, 40% of graph edges marked redundant but only 3.5% used, and overall moderate runtime overhead with occasional speedups.
AI-written summary · about
chapters (13)
- 0:00Congruence closure in SMT
- 1:47Equality saturation challenges
- 3:13Traditional congruence closure
- 6:23Greedy algorithm for explanations
- 8:08Weighted path selection
- 10:13Redundant edges for shortcuts
- 11:58SMT solver environment challenges
- 13:41Backtracking in SMT solvers
- 16:06Circular proof dependencies
- 17:49Experimental evaluation
- 19:34Performance impact findings
- 21:39Conclusion and future work
- 23:23Q&A
related talks
17mSatisfiability Algorithms Based on Concentrated Shrinkage
13mConsistency-Preserving Propagation for SMT Solving of Concurrent Program Verification
35mA Peek Inside SAT Solvers
40mReasoning Under Uncertainty in SMT Solving, Research, and Life
15mValidating SMT Rewriters via Rewrite Space Exploration Supported by Generative(…)
22mImplementing separation logic using an SMT-backed Frame Rule
21mMassive proofs for the masses
15mTowards Proof Stability in SMT-based Program Verification