Synthesizing MILP Constraints for Efficient and Robust Optimization
summary
Proposes a syntax-guided synthesis pipeline that generates MILP encodings from arbitrary Boolean-linear specs, implementing an extensible DSL, iterative decomposition to add decision variables, and over-/under-approximation checks to prune candidates. Prototype uses Lingride and Z3, runs on benchmarks from operations research, ML and Q&A posts, and reports synthesis times of seconds–minutes, DSL strengthening needed for ~70% of problems, and overall solver runtimes roughly matching or improving manual encodings (≈9% median speedup). conx-based splitting reduces relaxation size.
AI-written summary · about
chapters (13)
- 0:00Paper introduction
- 0:22Mixed integer linear programming
- 1:57MILP vs SMT solvers
- 2:39Linearizing logical constraints
- 3:21Synthesizing MILP constraints
- 4:25Protein folding example
- 5:50Proposed method overview
- 6:34DSL variable strengthening
- 9:05Pruning synthesis candidates
- 9:48Selecting high-quality constraints
- 11:35Experimental evaluation
- 13:43Summary and contributions
- 14:13Q&A
related talks
38mFusing Machine Learning and Mixed Integer Linear Programming
38mProgram Synthesis: A Dream Realized?
59mVerification and Machine Learning
17mAlgebro-geometric Algorithms for Template-Based Synthesis of Polynomial Program...
20mFunction synthesis for maximizing model counting
22mSynthesizing Efficiently Monitorable Formulas in Metric Temporal Logic
14mMulti-Language Probabilistic Programming
16mJust-in-Time Learning for Bottom-Up Enumerative Synthesis