Synthesizing MILP Constraints for Efficient and Robust Optimization
Synthesizing MILP Constraints for Efficient and Robust Optimization
复制标题
DOI：
10.1145/3591298
复制
发表时间：
2023-06
影响因子：
--
通讯作者：
Jingbo Wang;Aarti Gupta;Chao Wang
中科院分区：
文献类型：
--
作者：
Jingbo Wang;Aarti Gupta;Chao Wang
虽然混合整数线性规划（MILP）求解器通常用于解决各种重要的科学和工程问题，但对于最终用户来说，编写正确有效的MILP约束仍然是一项具有挑战性的任务，特别是对于使用固有的非线性布尔逻辑运算指定的问题。为了克服这一挑战，我们提出了一种语法引导合成（SyGuS）方法，能够从使用布尔逻辑运算的任意组合表示的规范中生成高质量的MILP约束。我们的方法的核心是一个可扩展的领域规范语言（DSL），它的表达能力可以通过添加新的整数变量作为决策变量，以及使用这些整数变量从非线性布尔逻辑操作合成线性约束的迭代过程来改进。为了使合成方法更有效，我们还提出了一种过度逼近技术来充分证明合成的线性约束的正确性，以及一种欠逼近技术来安全地修剪掉不正确的约束。我们已经在统计学、机器学习和数据科学应用的广泛基准规范上实现和评估了该方法。实验结果表明，该方法在处理这些基准测试中是有效的，并且合成的MILP约束的质量在紧凑性和求解时间方面接近或高于手动编写的约束。
While mixed integer linear programming (MILP) solvers are routinely used to solve a wide range of important science and engineering problems, it remains a challenging task for end users to write correct and efficient MILP constraints, especially for problems specified using the inherently non-linear Boolean logic operations. To overcome this challenge, we propose a syntax guided synthesis (SyGuS) method capable of generating high-quality MILP constraints from the specifications expressed using arbitrary combinations of Boolean logic operations. At the center of our method is an extensible domain specification language (DSL) whose expressiveness may be improved by adding new integer variables as decision variables, together with an iterative procedure for synthesizing linear constraints from non-linear Boolean logic operations using these integer variables. To make the synthesis method efficient, we also propose an over-approximation technique for soundly proving the correctness of the synthesized linear constraints, and an under-approximation technique for safely pruning away the incorrect constraints. We have implemented and evaluated the method on a wide range of benchmark specifications from statistics, machine learning, and data science applications. The experimental results show that the method is efficient in handling these benchmarks, and the quality of the synthesized MILP constraints is close to, or higher than, that of manually-written constraints in terms of both compactness and solving time.