Structure-guided Local Improvement for Maximum Satisfiability
summary
Presents a method that iteratively extracts tiny subinstances by growing a frontier from unsatisfied soft clauses on the primal graph expansion, fixes the rest as assumptions, and hands each local problem to a complete solver (experiment uses MaxHS-in-loop) to seek local improvements. Benchmarks show more instances improved than standard LNS—especially weighted cases—and gains grow with longer runs, though average score sometimes trails the best incomplete solver; main bottleneck is repeatedly instantiating subcalls instead of using incremental MaxSAT.
AI-written summary · about
chapters (7)
- 0:00Start
- 1:32SAT-based Local Improvement (SLIM)
- 3:24SLIM for MaxSAT Local Instances
- 4:35Example
- 5:27Primal Graph
- 17:43Conclusion
- 18:32Open Questions
related talks
16mSoftware Model Checking via Summary-Guided Search
21mBounded-Exhaustive Subspace Diversification for SMT Solver Testing
17mFinding Adversarial Inputs for Heuristics using Multi-level Optimization
40mUtilizing Structure in Combinatorial Solving and Reasoning
31mGenerating Constraint Programs for Variability Model Reasoning: A DSL and Solver-...
15mHieraSynth: A Parallel Framework for Complete Super-Optimization with Hierarchical(…)
19mBeyond Affine Loops: A Geometric Approach to Program Synthesis
01h 09mPlenary: Neighborhoods Banding Together: Reasoning Globally about Programs