{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T22:00:53Z","timestamp":1747173653907,"version":"3.40.5"},"reference-count":22,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2020,9,22]],"date-time":"2020-09-22T00:00:00Z","timestamp":1600732800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2020,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Cooperation among constraint solvers is difficult because different solving paradigms have different theoretical foundations. Recent works have shown that abstract interpretation can provide a unifying theory for various constraint solvers. In particular, it relies on abstract domains which capture constraint languages as ordered structures. The key insight of this paper is viewing cooperation schemes as abstract domains combinations. We propose a modular framework in which solvers and cooperation schemes can be seamlessly added and combined. This differs from existing approaches such as SMT where the cooperation scheme is usually fixed (<jats:italic>e.g.<\/jats:italic>, Nelson-Oppen). We contribute to two new cooperation schemes: (i)<jats:italic>interval propagators completion<\/jats:italic>that allows abstract domains to exchange bound constraints, and (ii)<jats:italic>delayed product<\/jats:italic>which exchanges over-approximations of constraints between two abstract domains. Moreover, the delayed product is based on delayed goal of logic programming, and it shows that abstract domains can also capture control aspects of constraint solving. Finally, to achieve modularity, we propose the<jats:italic>shared product<\/jats:italic>to combine abstract domains and cooperation schemes. Our approach has been fully implemented, and we provide various examples on the flexible job shop scheduling problem.<\/jats:p>","DOI":"10.1017\/s1471068420000162","type":"journal-article","created":{"date-parts":[[2020,9,22]],"date-time":"2020-09-22T02:43:15Z","timestamp":1600742595000},"page":"848-863","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":1,"title":["Modular Constraint Solver Cooperation via Abstract Interpretation"],"prefix":"10.1017","volume":"20","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9202-4541","authenticated-orcid":false,"given":"PIERRE","family":"TALBOT","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"\u00c9RIC","family":"MONFROY","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"CHARLOTTE","family":"TRUCHET","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2020,9,22]]},"reference":[{"key":"S1471068420000162_ref22","doi-asserted-by":"crossref","unstructured":"22. Ziat, G. , Mar\u00e9chal, A. , Marie, P. , Min\u00e9, A. , and Truchet, C. 2019. Combination of Boxes and Polyhedra Abstractions for Constraint Solving. In NSAD \u201919.","DOI":"10.1007\/978-3-030-54997-8_8"},{"key":"S1471068420000162_ref9","doi-asserted-by":"crossref","unstructured":"9. Fern\u00e1ndez, A. J. and Hill, P. M. 2004. An interval constraint system for lattice domains. ACM Trans. Program. Lang. Syst. 26, 1 (Jan.), 1\u201346. https:\/\/doi.org\/10.1145\/963778.963779.","DOI":"10.1145\/963778.963779"},{"key":"S1471068420000162_ref3","doi-asserted-by":"crossref","unstructured":"3. Brand, S. , Narodytska, N. , Quimper, C.-G. , Stuckey, P. , and Walsh, T. 2007. Encodings of the sequence constraint. In CP \u201907. Springer, 210\u2013224. https:\/\/doi.org\/10.1007\/978-3-540-74970-7_17.","DOI":"10.1007\/978-3-540-74970-7_17"},{"key":"S1471068420000162_ref20","doi-asserted-by":"crossref","unstructured":"20. Talbot, P. , Cachera, D. , Monfroy, E. , and Truchet, C. 2019. Combining Constraint Languages via Abstract Interpretation. In ICTAI \u201919. 50\u201358. https:\/\/doi.org\/10.1109\/ICTAI.2019.00016.","DOI":"10.1109\/ICTAI.2019.00016"},{"key":"S1471068420000162_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-008-9064-x"},{"key":"S1471068420000162_ref11","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","article-title":"The octagon abstract domain","volume":"1","author":"Min\u00e9","year":"2006","journal-title":"Higher-Order and Symbolic Computation (HOSC) 19"},{"key":"S1471068420000162_ref21","doi-asserted-by":"crossref","unstructured":"21. Talbot, P. , \u00c9ric, Monfroy , and Truchet, C. 2020. Modular constraint solver cooperation via abstract interpretation. http:\/\/arxiv.org\/abs\/2008.01415.","DOI":"10.1017\/S1471068420000162"},{"key":"S1471068420000162_ref7","doi-asserted-by":"crossref","unstructured":"7. D\u2019Silva, V. , Haller, L. , and Kroening, D. 2014. Abstract satisfaction. In POPL \u201914. ACM Press, 139\u2013150. https:\/\/doi.org\/10.1145\/2535838.2535868.","DOI":"10.1145\/2535838.2535868"},{"key":"S1471068420000162_ref4","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/BF02238804","article-title":"Job-shop scheduling with multi-purpose machines","volume":"4","author":"Brucker","year":"1990","journal-title":"Computing 45"},{"key":"S1471068420000162_ref5","doi-asserted-by":"crossref","unstructured":"5. Cousot, P. and Cousot, R. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL \u201977. ACM, 238\u2013252. https:\/\/doi.org\/10.1145\/512950.512973.","DOI":"10.1145\/512950.512973"},{"key":"S1471068420000162_ref6","first-page":"31","article-title":"Theories, solvers and static analysis by abstract interpretation","volume":"6","author":"Cousot","year":"2012","journal-title":"Journal of the ACM (JACM) 59"},{"key":"S1471068420000162_ref10","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1007\/BF01719451","article-title":"Tabu search for the job-shop scheduling problem with multi-purpose machines","volume":"4","author":"Hurink","year":"1994","journal-title":"Operations-Research-Spektrum 15"},{"key":"S1471068420000162_ref17","unstructured":"17. Schulte, C. , Tack, G. , and Lagerkvist, M. 2019. Modeling and Programming with Gecode."},{"key":"S1471068420000162_ref18","doi-asserted-by":"crossref","unstructured":"18. Schutt, A. , Feydy, T. , and Stuckey, P. 2013. Scheduling optional tasks with explanation. In CP\u201913. 628\u2013644. https:\/\/doi.org\/10.1007\/978-3-642-40627-0_47.","DOI":"10.1007\/978-3-642-40627-0_47"},{"volume-title":"Verification, Model Checking, and Abstract Interpretation","year":"2013","author":"Pelleau","key":"S1471068420000162_ref16"},{"key":"S1471068420000162_ref19","doi-asserted-by":"crossref","unstructured":"19. Talbot, P. 2019. Spacetime Programming: A Synchronous Language for Composable Search Strategies. In PPDP \u201919. 18:1\u201318:16. https:\/\/doi.org\/10.1145\/3354166.3354183.","DOI":"10.1145\/3354166.3354183"},{"key":"S1471068420000162_ref2","doi-asserted-by":"crossref","unstructured":"2. Benhamou, F. , Goualard, F. , Granvilliers, L. , and Puget, J.-F. 1999. Revising hull and box consistency. In Proceedings of the 1999 International Conference on Logic Programming. 230\u2013244. https:\/\/doi.org\/10.7551\/mitpress\/4304.003.0024.","DOI":"10.7551\/mitpress\/4304.003.0024"},{"key":"S1471068420000162_ref12","first-page":"1","article-title":"An environment for designing\/executing constraint solver collaborations","volume":"1","author":"Monfroy","year":"1998","journal-title":"Electronic Notes in Theoretical Computer Science 16"},{"key":"S1471068420000162_ref13","doi-asserted-by":"crossref","unstructured":"13. Nelson, G. and Oppen, D. C. 1979. Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1, 2, 245\u2013257. https:\/\/doi.org\/10.1145\/357073.357079.","DOI":"10.1145\/357073.357079"},{"key":"S1471068420000162_ref8","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068409003780"},{"key":"S1471068420000162_ref15","unstructured":"15. Older, W. 1993. Programming in CLP(BNR). In Position Papers for the First Workshop on Principles and Practice of Constraint Programming. 239\u2013249."},{"key":"S1471068420000162_ref1","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1016\/S0304-3975(99)00032-8","article-title":"The essence of constraint propagation","volume":"1","author":"Apt","year":"1999","journal-title":"Theoretical computer science 221"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068420000162","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,19]],"date-time":"2022-11-19T11:40:26Z","timestamp":1668858026000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068420000162\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9,22]]},"references-count":22,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2020,11]]}},"alternative-id":["S1471068420000162"],"URL":"https:\/\/doi.org\/10.1017\/s1471068420000162","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"type":"print","value":"1471-0684"},{"type":"electronic","value":"1475-3081"}],"subject":[],"published":{"date-parts":[[2020,9,22]]},"assertion":[{"value":"\u00a9 The Author(s), 2020. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}