Proof Logging for MaxSAT – The Past, The Present and The Future
summary
MaxSAT is effective but lacks mature proof logging; recent work uses SAT solvers plus pseudo-Boolean cutting planes and finds real bugs where solvers perform unsound reasoning yet returned optimal costs on all benchmarks. Common algorithms are core-guided and implicit-hitting (IHS); OLL-style core-guided logging is now implemented using VeriPB, while IHS needs proof logging for the MIP step. Extensions include MaxSAT resolution and RAT/PR-style redundancy rules; the challenge is combining SAT proofs with certified cost reasoning.
AI-written summary · about
chapters (10)
- 0:00Start
- 7:30Why not SAT proofs?
- 9:09What is needed for proof logging SAT-based MaxSAT?
- 13:33Checking SAT solvers
- 14:34Tableaux Calculus for MaxSAT
- 16:02Cost-aware clause redundancy notions
- 17:32MaxSAT Resolution
- 20:13Cutting Planes for logging SAT-based MaxSAT
- 21:47Future Directions & Challenges
- 23:38Summary