Certified Static and Dynamic Symmetry Breaking
summary
This work shows how to produce machine-verifiable certificates for both static symmetry breaking and a prototype of dynamic symmetry breaking by encoding lexicographic leader constraints and checking them with VeriPB proof logging. The key is a new dominance rule that treats symmetry fixing as an optimization (lexicographic) certificate, allowing independent certification of each generator. A student implemented the dynamic variant, found and fixed two real bugs, and the approach yields a general, practical method for arbitrary syntactic symmetries; extending DRAT or relating the rule to extended Frege remain open.
AI-written summary · about
chapters (13)
- 0:00Start
- 3:07INTRODUCTION
- 4:24SYMMETRY HANDLING TECHNIQUES
- 9:56CERTIFIED SYMMETRY HANDUNG
- 13:18THE VERIPB PROOF SYSTEM
- 15:10REDUNDANCE-BASED STRENGTHENING
- 18:20PROOF LOGGING FOR OPTIMIZATION PROBLEMS
- 19:58REDUNDANCE AND DOMINANCE RULES
- 20:57SOUNDNESS OF DOMINANCE RULE
- 22:29STRENGTH OF DOMINANCE RULE
- 26:04STRATEGY FOR SAT SYMMETRY BREAKING
- 27:18EXPERIMENTAL EVALUATION
- 28:43CONCLUSION
related talks
14mA Hoare Logic For Symmetry Properties
23mVerifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
20mFormal framework for reasoning about the precision of dynamic analysis
21mMechanised Hypersafety Proofs about Structured Data
24mRelational Symbolic Execution for Differential Privacy
17mCode-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into(…)
19mProof Automation for Linearizability in Separation Logic
21mThe Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs