{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,19]],"date-time":"2026-05-19T01:01:41Z","timestamp":1779152501530,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":48,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,8,18]],"date-time":"2021-08-18T00:00:00Z","timestamp":1629244800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Funda\u00e7\u00e3o para a Ci\u00eancia e Tecnologia","award":["PTDC\/CCI-COM\/31198\/2017,UIDB\/50021\/2020,PhD grant SFRH\/BD\/07724\/2020"],"award-info":[{"award-number":["PTDC\/CCI-COM\/31198\/2017,UIDB\/50021\/2020,PhD grant SFRH\/BD\/07724\/2020"]}]},{"DOI":"10.13039\/100000001","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["CCF-1918140,CNS-1801546,1762363"],"award-info":[{"award-number":["CCF-1918140,CNS-1801546,1762363"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100009226","name":"National Security Agency","doi-asserted-by":"publisher","award":["H9823018D0008"],"award-info":[{"award-number":["H9823018D0008"]}],"id":[{"id":"10.13039\/100009226","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014172889"],"award-info":[{"award-number":["N00014172889"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,8,20]]},"DOI":"10.1145\/3468264.3468587","type":"proceedings-article","created":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T01:40:37Z","timestamp":1629337237000},"page":"155-167","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["AlloyMax: bringing maximum satisfaction to relational specifications"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1689-6633","authenticated-orcid":false,"given":"Changjian","family":"Zhang","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ryan","family":"Wagner","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pedro","family":"Orvalho","sequence":"additional","affiliation":[{"name":"INESC-ID, Portugal \/ University of Lisbon, Portugal"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Garlan","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vasco","family":"Manquinho","sequence":"additional","affiliation":[{"name":"INESC-ID, Portugal \/ University of Lisbon, Portugal"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ruben","family":"Martins","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eunsuk","family":"Kang","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,8,18]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2010.27"},{"key":"e_1_3_2_1_2_1","volume-title":"MaxSAT Evaluation 2020: Solver and Benchmark Descriptions","author":"Bacchus Fahiem","unstructured":"Fahiem Bacchus , Jeremias Berg , Matti J\u00e4rvisalo , and Ruben Martins . 2020. MaxSAT Evaluation 2020: Solver and Benchmark Descriptions . University of Helsinki , Department of Computer Science. Fahiem Bacchus, Jeremias Berg, Matti J\u00e4rvisalo, and Ruben Martins. 2020. MaxSAT Evaluation 2020: Solver and Benchmark Descriptions. University of Helsinki, Department of Computer Science."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.3233\/FAIA201008"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19249-9_6"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_14"},{"key":"e_1_3_2_1_6_1","volume-title":"Answer Set Optimization. In International Joint Conference on Artificial Intelligence (IJCAI), Georg Gottlob and Toby Walsh (Eds.).","author":"Brewka Gerhard","year":"2003","unstructured":"Gerhard Brewka , Ilkka Niemel\u00e4 , and Miroslaw Truszczynski . 2003 . Answer Set Optimization. In International Joint Conference on Artificial Intelligence (IJCAI), Georg Gottlob and Toby Walsh (Eds.). Gerhard Brewka, Ilkka Niemel\u00e4, and Miroslaw Truszczynski. 2003. Answer Set Optimization. In International Joint Conference on Artificial Intelligence (IJCAI), Georg Gottlob and Toby Walsh (Eds.)."},{"key":"e_1_3_2_1_7_1","volume-title":"Logic Programming and Databases","author":"Ceri Stefano","year":"2059","unstructured":"Stefano Ceri , Georg Gottlob , and Letizia Tanca . 1990. Logic Programming and Databases . Springer . isbn:3-540-51728-6 https:\/\/www.worldcat.org\/oclc\/ 2059 5273 Stefano Ceri, Georg Gottlob, and Letizia Tanca. 1990. Logic Programming and Databases. Springer. isbn:3-540-51728-6 https:\/\/www.worldcat.org\/oclc\/20595273"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54804-8_2"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146251"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2017.23379"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-6800-5_7"},{"key":"e_1_3_2_1_12_1","unstructured":"Gurobi Optimization. 2021. Gurobi Optimizer Reference Manual. http:\/\/www.gurobi.com  Gurobi Optimization. 2021. Gurobi Optimizer Reference Manual. http:\/\/www.gurobi.com"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/71.80192"},{"key":"e_1_3_2_1_14_1","unstructured":"International Business Machines Corporation (IBM). 2009. V12. 1: User\u2019s Manual for CPLEX.  International Business Machines Corporation (IBM). 2009. V12. 1: User\u2019s Manual for CPLEX."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/355045.355063"},{"key":"e_1_3_2_1_16_1","volume-title":"Software Abstractions: Logic, language, and analysis","author":"Jackson Daniel","year":"2006","unstructured":"Daniel Jackson . 2006 . Software Abstractions: Logic, language, and analysis . MIT Press . isbn:9780262101141 Daniel Jackson. 2006. Software Abstractions: Logic, language, and analysis. MIT Press. isbn:9780262101141"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/347324.383378"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950356"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:AUSE.0000038938.10589.b9"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00002"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535857"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29908-8_49"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-24658-7"},{"key":"e_1_3_2_1_24_1","unstructured":"Moritz Lipp Michael Schwarz Daniel Gruss Thomas Prescher Werner Haas Stefan Mangard Paul Kocher Daniel Genkin Yuval Yarom and Mike Hamburg. 2018. Meltdown. arxiv:1801.01207.  Moritz Lipp Michael Schwarz Daniel Gruss Thomas Prescher Werner Haas Stefan Mangard Paul Kocher Daniel Genkin Yuval Yarom and Mike Hamburg. 2018. Meltdown. arxiv:1801.01207."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2014.38"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63516-3_3"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43652-3_31"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-98334-9_21"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-011-9233-2"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39071-5_14"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-09284-3_33"},{"key":"e_1_3_2_1_32_1","volume-title":"Lisbon Wedding: Seating arrangements using MaxSAT. MaxSAT Evaluation 2017 : Solver and Benchmark Descriptions, B-2017-2","author":"Martins Ruben","year":"2017","unstructured":"Ruben Martins and Justine Sherry . 2017 . Lisbon Wedding: Seating arrangements using MaxSAT. MaxSAT Evaluation 2017 : Solver and Benchmark Descriptions, B-2017-2 (2017), 25. Ruben Martins and Justine Sherry. 2017. Lisbon Wedding: Seating arrangements using MaxSAT. MaxSAT Evaluation 2017 : Solver and Benchmark Descriptions, B-2017-2 (2017), 25."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2015.77"},{"key":"e_1_3_2_1_34_1","volume-title":"USENIX Conference on Systems Administration (LISA). 155\u2013168","author":"Narain Sanjai","year":"2005","unstructured":"Sanjai Narain . 2005 . Network Configuration Management via Model Finding . In USENIX Conference on Systems Administration (LISA). 155\u2013168 . Sanjai Narain. 2005. Network Configuration Management via Model Finding. In USENIX Conference on Systems Administration (LISA). 155\u2013168."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606569"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74970-7_38"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24318-4_20"},{"key":"e_1_3_2_1_38_1","unstructured":"2006. Handbook of Constraint Programming Francesca Rossi Peter van Beek and Toby Walsh (Eds.) (Foundations of Artificial Intelligence Vol. 2). Elsevier.  2006. Handbook of Constraint Programming Francesca Rossi Peter van Beek and Toby Walsh (Eds.) (Foundations of Artificial Intelligence Vol. 2). Elsevier."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-09508-6"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380365"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_49"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2018.00081"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38706-7_10"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/tdsc.2013.24"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2017.2655056"},{"key":"e_1_3_2_1_48_1","volume-title":"Proceedings of the AAAI Conference on Artificial Intelligence, 26","author":"Zhang Lei","year":"2012","unstructured":"Lei Zhang and Fahiem Bacchus . 2012 . MAXSAT Heuristics for Cost Optimal Planning . Proceedings of the AAAI Conference on Artificial Intelligence, 26 , 1 (2012), Jul., https:\/\/ojs.aaai.org\/index.php\/AAAI\/article\/view\/8373 Lei Zhang and Fahiem Bacchus. 2012. MAXSAT Heuristics for Cost Optimal Planning. Proceedings of the AAAI Conference on Artificial Intelligence, 26, 1 (2012), Jul., https:\/\/ojs.aaai.org\/index.php\/AAAI\/article\/view\/8373"}],"event":{"name":"ESEC\/FSE '21: 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","location":"Athens Greece","acronym":"ESEC\/FSE '21","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3468264.3468587","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3468264.3468587","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3468264.3468587","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:24:51Z","timestamp":1750195491000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3468264.3468587"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,18]]},"references-count":48,"alternative-id":["10.1145\/3468264.3468587","10.1145\/3468264"],"URL":"https:\/\/doi.org\/10.1145\/3468264.3468587","relation":{},"subject":[],"published":{"date-parts":[[2021,8,18]]},"assertion":[{"value":"2021-08-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}