Explore a 17-minute conference talk from PLDI 2023 that introduces a syntax guided synthesis (SyGuS) method for generating high-quality mixed integer linear programming (MILP) constraints. Learn how this innovative approach tackles the challenge of writing correct and efficient MILP constraints for problems specified using non-linear Boolean logic operations. Discover the extensible domain specification language (DSL) at the core of the method, which improves expressiveness by adding new integer variables as decision variables. Understand the iterative procedure for synthesizing linear constraints from non-linear Boolean logic operations and the techniques used to enhance synthesis efficiency, including over-approximation for correctness proofs and under-approximation for pruning incorrect constraints. Gain insights into the method's performance on benchmark specifications from statistics, machine learning, and data science applications, and compare the quality of synthesized MILP constraints to manually-written ones in terms of compactness and solving time.
Overview
Syllabus
[PLDI'23] Synthesizing MILP Constraints for Efficient and Robust Optimization
Taught by
ACM SIGPLAN