{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T23:15:41Z","timestamp":1773875741161,"version":"3.50.1"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T00:00:00Z","timestamp":1686009600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"U.S. National Science Foundation grant","award":["CCF-2220345"],"award-info":[{"award-number":["CCF-2220345"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,6,6]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/3591298","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"1896-1919","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Synthesizing MILP Constraints for Efficient and Robust Optimization"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5877-2677","authenticated-orcid":false,"given":"Jingbo","family":"Wang","sequence":"first","affiliation":[{"name":"University of Southern California, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6676-9400","authenticated-orcid":false,"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[{"name":"Princeton University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-4684-3943","authenticated-orcid":false,"given":"Chao","family":"Wang","sequence":"additional","affiliation":[{"name":"University of Southern California, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v33i01.33011418"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_18"},{"key":"e_1_2_1_4_1","first-page":"1441","article-title":"Disjunctive inequalities: applications and extensions","volume":"2","author":"Belotti Pietro","year":"2011","unstructured":"Pietro Belotti , Leo Liberti , Andrea Lodi , Giacomo Nannicini , and Andrea Tramontani . 2011 . Disjunctive inequalities: applications and extensions . Wiley Encyclopedia of Operations Research and Management Science , 2 (2011), 1441 \u2013 1450 . Pietro Belotti, Leo Liberti, Andrea Lodi, Giacomo Nannicini, and Andrea Tramontani. 2011. Disjunctive inequalities: applications and extensions. Wiley Encyclopedia of Operations Research and Management Science, 2 (2011), 1441\u20131450.","journal-title":"Wiley Encyclopedia of Operations Research and Management Science"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1137\/20M1346778"},{"key":"e_1_2_1_6_1","first-page":"13","article-title":"Solving Large-Scale Sparse PCA to Certifiable (Near) Optimality","volume":"23","author":"Bertsimas Dimitris","year":"2022","unstructured":"Dimitris Bertsimas , Ryan Cory-Wright , and Jean Pauphilet . 2022 . Solving Large-Scale Sparse PCA to Certifiable (Near) Optimality .. J. Mach. Learn. Res. , 23 (2022), 13 \u2013 11 . Dimitris Bertsimas, Ryan Cory-Wright, and Jean Pauphilet. 2022. Solving Large-Scale Sparse PCA to Certifiable (Near) Optimality.. J. Mach. Learn. Res., 23 (2022), 13\u20131.","journal-title":"J. Mach. Learn. Res."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10994-017-5633-9"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1214\/18-AOS1804"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1137\/141000671"},{"key":"e_1_2_1_10_1","first-page":"159","article-title":"The gurobi optimizer","volume":"41","author":"Bixby Bob","year":"2007","unstructured":"Bob Bixby . 2007 . The gurobi optimizer . Transp. Re-search Part B , 41 , 2 (2007), 159 \u2013 178 . Bob Bixby. 2007. The gurobi optimizer. Transp. Re-search Part B, 41, 2 (2007), 159\u2013178.","journal-title":"Transp. Re-search Part B"},{"key":"e_1_2_1_11_1","volume-title":"USENIX Security Symposium. 643\u2013659","author":"Blazytko Tim","year":"2017","unstructured":"Tim Blazytko , Moritz Contag , Cornelius Aschermann , and Thorsten Holz . 2017 . Syntia: Synthesizing the Semantics of Obfuscated Code .. In USENIX Security Symposium. 643\u2013659 . https:\/\/doi.org\/10.5555\/3241189.3241240 10.5555\/3241189.3241240 Tim Blazytko, Moritz Contag, Cornelius Aschermann, and Thorsten Holz. 2017. Syntia: Synthesizing the Semantics of Obfuscated Code.. In USENIX Security Symposium. 643\u2013659. https:\/\/doi.org\/10.5555\/3241189.3241240"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.776041"},{"key":"e_1_2_1_13_1","unstructured":"Allison Chang Dimitris Bertsimas and Cynthia Rudin. 2012. An integer optimization approach to associative classification. In Advances in neural information processing systems. 269\u2013277. \t\t\t\t  Allison Chang Dimitris Bertsimas and Cynthia Rudin. 2012. An integer optimization approach to associative classification. In Advances in neural information processing systems. 269\u2013277."},{"key":"e_1_2_1_14_1","volume-title":"Integer optimization methods for machine learning. Ph. D. Dissertation","author":"Chang Allison An","unstructured":"Allison An Chang . 2012. Integer optimization methods for machine learning. Ph. D. Dissertation . Massachusetts Institute of Technology . https:\/\/doi.org\/1721.1\/72643 Allison An Chang. 2012. Integer optimization methods for machine learning. Ph. D. Dissertation. Massachusetts Institute of Technology. https:\/\/doi.org\/1721.1\/72643"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11590-020-01644-6"},{"key":"e_1_2_1_16_1","volume-title":"Manual for CPLEX","author":"IBM ILOG","year":"2015","unstructured":"IBM ILOG CPLEX. 2015 . V12. 6 User\u2019s Manual for CPLEX 2015. CPLEX division. IBM ILOG CPLEX. 2015. V12. 6 User\u2019s Manual for CPLEX 2015. CPLEX division."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-020-09318-x"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_8"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_19"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2020.findings-emnlp.56"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192382"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062351"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737977"},{"key":"e_1_2_1_24_1","volume-title":"Quadratic binary programming models in computational biology. Algorithmic Operations Research, 3, 2","author":"Forrester Richard John","year":"2008","unstructured":"Richard John Forrester and Harvey J Greenberg . 2008. Quadratic binary programming models in computational biology. Algorithmic Operations Research, 3, 2 ( 2008 ). Richard John Forrester and Harvey J Greenberg. 2008. Quadratic binary programming models in computational biology. Algorithmic Operations Research, 3, 2 (2008)."},{"key":"e_1_2_1_25_1","volume-title":"5th INFORMS Optimization Society Conference. 6\u20138March.","author":"Fourer Robert","year":"2014","unstructured":"Robert Fourer . 2014 . Strategies for not linear optimization . In 5th INFORMS Optimization Society Conference. 6\u20138March. Robert Fourer. 2014. Strategies for not linear optimization. In 5th INFORMS Optimization Society Conference. 6\u20138March."},{"key":"e_1_2_1_26_1","volume-title":"AMPL: A mathematical programming language. AT & T Bell Laboratories Murray Hill, NJ.","author":"Fourer Robert","year":"1987","unstructured":"Robert Fourer , David M Gay , and Brian W Kernighan . 1987 . AMPL: A mathematical programming language. AT & T Bell Laboratories Murray Hill, NJ. Robert Fourer, David M Gay, and Brian W Kernighan. 1987. AMPL: A mathematical programming language. AT & T Bell Laboratories Murray Hill, NJ."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837629"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1287\/mnsc.22.4.455"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371080"},{"key":"e_1_2_1_30_1","unstructured":"LLC Gurobi Optimization. 2018. Gurobi optimizer reference manual. \t\t\t\t  LLC Gurobi Optimization. 2018. Gurobi optimizer reference manual."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_18"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385979"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2014.6987606"},{"key":"e_1_2_1_34_1","first-page":"202","article-title":"Scaling up the accuracy of naive-bayes classifiers: A decision-tree hybrid","volume":"96","author":"Kohavi Ron","year":"1996","unstructured":"Ron Kohavi . 1996 . Scaling up the accuracy of naive-bayes classifiers: A decision-tree hybrid .. In Kdd. 96 , 202 \u2013 207 . Ron Kohavi. 1996. Scaling up the accuracy of naive-bayes classifiers: A decision-tree hybrid.. In Kdd. 96, 202\u2013207.","journal-title":"Kdd."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434335"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375696.1375702"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-86890-1_16"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1093\/bioinformatics\/btu022"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.patrec.2016.01.004"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_41_1","unstructured":"Pierluigi Nuzzo Alberto Puggelli Sanjit A Seshia and Alberto Sangiovanni-Vincentelli. 2010. CalCS: SMT solving for non-linear convex constraints. In Formal Methods in Computer Aided Design. 71\u201379. \t\t\t\t  Pierluigi Nuzzo Alberto Puggelli Sanjit A Seshia and Alberto Sangiovanni-Vincentelli. 2010. CalCS: SMT solving for non-linear convex constraints. In Formal Methods in Computer Aided Design. 71\u201379."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738007"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_8"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_19"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2980983.2908093"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_5"},{"key":"e_1_2_1_47_1","unstructured":"Junfu Shen and Jiang Ming. 2021. Mba-blast: unveiling and simplifying mixed boolean-arithmetic obfuscation. \t\t\t\t  Junfu Shen and Jiang Ming. 2021. Mba-blast: unveiling and simplifying mixed boolean-arithmetic obfuscation."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2018.2849003"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509578.2509586"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13188-2_18"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE43902.2021.00079"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158151"},{"key":"e_1_2_1_53_1","volume-title":"Model building in mathematical programming","author":"Williams H Paul","unstructured":"H Paul Williams . 2013. Model building in mathematical programming . John Wiley & Sons . H Paul Williams. 2013. Model building in mathematical programming. John Wiley & Sons."},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77535-5_5"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591298","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591298","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:21Z","timestamp":1750178841000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591298"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":54,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591298"],"URL":"https:\/\/doi.org\/10.1145\/3591298","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,6]]},"assertion":[{"value":"2023-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}