{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:14:11Z","timestamp":1762460051794,"version":"3.40.5"},"reference-count":47,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2021,11,9]],"date-time":"2021-11-09T00:00:00Z","timestamp":1636416000000},"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":[[2023,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Formal reasoning about finite sets and cardinality is important for many applications, including software verification, where very often one needs to reason about the size of a given data structure. The Constraint Logic Programming tool <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S1471068421000521_inline1.png\"\/><jats:tex-math>\n$$\\{ log\\} $$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> provides a decision procedure for deciding the satisfiability of formulas involving very general forms of finite sets, although it does not provide cardinality constraints. In this paper we adapt and integrate a decision procedure for a theory of finite sets with cardinality into <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S1471068421000521_inline1.png\"\/><jats:tex-math>\n$$\\{ log\\} $$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>. The proposed solver is proved to be a decision procedure for its formulas. Besides, the new CLP instance is implemented as part of the <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S1471068421000521_inline1.png\"\/><jats:tex-math>\n$$\\{ log\\} $$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> tool. In turn, the implementation uses Howe and King\u2019s Prolog SAT solver and Prolog\u2019s CLP(Q) library, as an integer linear programming solver. The empirical evaluation of this implementation based on +250 real verification conditions shows that it can be useful in practice.<\/jats:p><jats:p><jats:italic>Under consideration in Theory and Practice of Logic Programming (TPLP)<\/jats:italic><\/jats:p>","DOI":"10.1017\/s1471068421000521","type":"journal-article","created":{"date-parts":[[2021,11,9]],"date-time":"2021-11-09T05:19:41Z","timestamp":1636435181000},"page":"468-502","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":6,"title":["Integrating Cardinality Constraints into Constraint Logic Programming with Sets"],"prefix":"10.1017","volume":"23","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9163-2609","authenticated-orcid":false,"given":"MAXIMILIANO","family":"CRISTI\u00c1","sequence":"first","affiliation":[]},{"given":"GIANFRANCO","family":"ROSSI","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2021,11,9]]},"reference":[{"key":"S1471068421000521_ref17","doi-asserted-by":"crossref","unstructured":"Cristi\u00e1, M. , Rossi, G. and Frydman, C. S. 2013. {log} as a test case generator for the Test Template Framework. In SEFM, Hierons, R. M. , Merayo, M. G. , and Bravetti, M. , Eds. Lecture Notes in Computer Science, vol. 8137. Springer, 229\u2013243.","DOI":"10.1007\/978-3-642-40561-7_16"},{"key":"S1471068421000521_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/BF00137870"},{"key":"S1471068421000521_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-006-9042-1"},{"key":"S1471068421000521_ref47","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-005-3075-8"},{"key":"S1471068421000521_ref30","doi-asserted-by":"crossref","unstructured":"Kisby, C. , Blanco, S. , Kruckman, A. and Moss, L. S. 2020. Logics for sizes with union or intersection. In The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020. AAAI Press, 2870\u20132876.","DOI":"10.1609\/aaai.v34i03.5677"},{"key":"S1471068421000521_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-017-0279-6"},{"key":"S1471068421000521_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-006-9012-6"},{"key":"S1471068421000521_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(95)00147-6"},{"key":"S1471068421000521_ref38","doi-asserted-by":"crossref","unstructured":"Saaltink, M. 1997. The Z\/EVES system. In ZUM, Bowen, J. P. , Hinchey, M. G. , and Till, D. , Eds. Lecture Notes in Computer Science, vol. 1212. Springer, 72\u201385.","DOI":"10.1007\/BFb0027284"},{"key":"S1471068421000521_ref22","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068406002730"},{"key":"S1471068421000521_ref42","doi-asserted-by":"crossref","unstructured":"Suter, P. , Steiger, R. and Kuncak, V. 2011. Sets with cardinality constraints in satisfiability modulo theories. In Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings, Jhala, R. and Schmidt, D. A. , Eds. Lecture Notes in Computer Science, vol. 6538. Springer, 403\u2013418.","DOI":"10.1007\/978-3-642-18275-4_28"},{"key":"S1471068421000521_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-92280-5_3"},{"key":"S1471068421000521_ref46","doi-asserted-by":"crossref","unstructured":"Zarba, C. G. 2002b. Combining sets with integers. In Frontiers of Combining Systems, 4th International Workshop, FroCoS 2002, Santa Margherita Ligure, Italy, April 8-10, 2002, Proceedings, Armando, A , Ed. Lecture Notes in Computer Science, vol. 2309. Springer, 103\u2013116.","DOI":"10.1007\/3-540-45988-X_9"},{"key":"S1471068421000521_ref27","unstructured":"Hibti, M. 1995. D\u00e9cidabilit\u00e9 et complexit\u00e9 de syst\u00e8mes de contraintes ensemblistes. Ph.D. thesis. Th\u00e8se de doctorat dirig\u00e9e par Lombardi, Henri Sciences appliqu\u00e9es Besan\u00e7on 1995."},{"key":"S1471068421000521_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09520-4"},{"key":"S1471068421000521_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-021-09602-2"},{"key":"S1471068421000521_ref24","unstructured":"Gervet, C. 1994. Conjunto: Constraint propagation over set constraints with finite set domain variables. In ICLP, Hentenryck, P. V , Ed. MIT Press, 733."},{"key":"S1471068421000521_ref7","doi-asserted-by":"crossref","unstructured":"Bradley, A. R. , Manna, Z. and Sipma, H. B. 2006. What\u2019s decidable about arrays? In Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8\u201310, 2006, Proceedings, Emerson, E. A. and Namjoshi, K. S. , Eds. Lecture Notes in Computer Science, vol. 3855. Springer, 427\u2013442.","DOI":"10.1007\/11609773_28"},{"key":"S1471068421000521_ref18","doi-asserted-by":"crossref","unstructured":"Dal Pal\u00fa, A. , Dovier, A. , Pontelli, E. and Rossi, G. 2003. Integrating finite domain constraints and CLP with sets. In Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declaritive Programming. PPDP \u201903. ACM, New York, NY, USA, 219\u2013229.","DOI":"10.1145\/888251.888272"},{"key":"S1471068421000521_ref34","doi-asserted-by":"crossref","unstructured":"Piskac, R. 2020. Efficient automated reasoning about sets and multisets with cardinality constraints. In Automated Reasoning \u2013 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I, Peltier, N. and Sofronie-Stokkermans, V. , Eds. Lecture Notes in Computer Science, vol. 12166. Springer, 3\u201310.","DOI":"10.1007\/978-3-030-51074-9_1"},{"key":"S1471068421000521_ref33","doi-asserted-by":"crossref","unstructured":"Levatich, M. , Bj\u00f8rner, N. , Piskac, R. and Shoham, S. 2020. Solving LIA* using approximations. In Verification, Model Checking, and Abstract Interpretation \u2013 21st International Conference, VMCAI 2020, New Orleans, LA, USA, January 16-21, 2020, Proceedings, Beyer, D. and Zufferey, D. , Eds. Lecture Notes in Computer Science, vol. 11990. Springer, 360\u2013378.","DOI":"10.1007\/978-3-030-39322-9_17"},{"key":"S1471068421000521_ref19","first-page":"1","article-title":"The logic of comparative cardinality","author":"Ding","year":"2020","journal-title":"J. Symb. Log."},{"key":"S1471068421000521_ref23","doi-asserted-by":"crossref","unstructured":"Ferro, A. , Omodeo, E. G. and Schwartz, J. T. 1980. Decision procedures for some fragments of set theory. In CADE, Bibel, W. and Kowalski, R. A. , Eds. Lecture Notes in Computer Science, vol. 87. Springer, 88\u201396.","DOI":"10.1007\/3-540-10009-1_8"},{"key":"S1471068421000521_ref10","doi-asserted-by":"crossref","unstructured":"Cristi\u00e1, M. and Rossi, G. 2017. A decision procedure for restricted intensional sets. In Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6\u201311, 2017, Proceedings, de Moura, L. , Ed. Lecture Notes in Computer Science, vol. 10395. Springer, 185\u2013201.","DOI":"10.1007\/978-3-319-63046-5_12"},{"key":"S1471068421000521_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"S1471068421000521_ref12","unstructured":"Cristi\u00e1, M. and Rossi, G. 2019. Rewrite rules for a solver for sets, binary relations and partial functions. Tech. rep. http:\/\/people.dmi.unipr.it\/gianfranco.rossi\/SETLOG\/calculus.pdf."},{"key":"S1471068421000521_ref40","unstructured":"Stuckey, P. J. , Marriott, K. and Tack, G. 2020. The MiniZinc Handbook. Tech. rep. https:\/\/www.minizinc.org\/doc-2.5.3\/en\/index.html."},{"key":"S1471068421000521_ref4","first-page":"4","article-title":"Reasoning with finite sets and cardinality constraints in SMT","author":"Bansal","year":"2018","journal-title":"Log. Methods Comput. Sci. 14,"},{"key":"S1471068421000521_ref26","doi-asserted-by":"publisher","DOI":"10.1613\/jair.1638"},{"key":"S1471068421000521_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-021-09589-w"},{"key":"S1471068421000521_ref9","unstructured":"Clearsy. Atelier B home page. http:\/\/www.atelierb.eu\/."},{"key":"S1471068421000521_ref32","doi-asserted-by":"crossref","unstructured":"Leuschel, M. and Butler, M. 2003. ProB: A model checker for B. In FME, Keijiro, A. , Gnesi, S. , and Mandrioli, D. , Eds. Lecture Notes in Computer Science, vol. 2805. Springer-Verlag, 855\u2013874.","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"S1471068421000521_ref44","doi-asserted-by":"crossref","unstructured":"Yessenov, K. , Piskac, R. and Kuncak, V. 2010. Collections, cardinalities, and relations. In Verification, Model Checking, and Abstract Interpretation, 11th International Conference, VMCAI 2010, Madrid, Spain, January 17\u201319, 2010. Proceedings, Barthe, G. and Hermenegildo, M. V. , Eds. Lecture Notes in Computer Science, vol. 5944. Springer, 380\u2013395.","DOI":"10.1007\/978-3-642-11319-2_27"},{"key":"S1471068421000521_ref36","doi-asserted-by":"crossref","unstructured":"Piskac, R. and Kuncak, V. 2010. MUNCH \u2013 Automated reasoner for sets and multisets. In Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16\u201319, 2010. Proceedings, Giesl, J. and H\u00e4hnle, R. , Eds. Lecture Notes in Computer Science, vol. 6173. Springer, 149\u2013155.","DOI":"10.1007\/978-3-642-14203-1_13"},{"key":"S1471068421000521_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2012.02.024"},{"key":"S1471068421000521_ref6","doi-asserted-by":"crossref","unstructured":"Berkovits, I. , Lazic, M. , Losa, G. , Padon, O. and Shoham, S. 2019. Verification of threshold-based distributed algorithms by decomposition to decidable logics. In Computer Aided Verification \u2013 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II, Dillig, I. and Tasiran, S. , Eds. Lecture Notes in Computer Science, vol. 11562. Springer, 245\u2013266.","DOI":"10.1007\/978-3-030-25543-5_15"},{"key":"S1471068421000521_ref11","doi-asserted-by":"crossref","unstructured":"Cristi\u00e1, M. and Rossi, G. 2018. A set solver for finite set relation algebra. In Relational and Algebraic Methods in Computer Science - 17th International Conference, RAMiCS 2018, Groningen, The Netherlands, October 29 - November 1, 2018, Proceedings, Desharnais, J. , Guttmann, W. , and Joosten, S. , Eds. Lecture Notes in Computer Science, vol. 11194. Springer, 333\u2013349.","DOI":"10.1007\/978-3-030-02149-8_20"},{"key":"S1471068421000521_ref28","unstructured":"Holzbaur, C. 1995. OFAI CLP(Q,R) manual. Tech. rep., edition 1.3.3. Technical Report TR-95-09, Austrian Research Institute for Artificial Intelligence."},{"key":"S1471068421000521_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/365151.365169"},{"key":"S1471068421000521_ref35","doi-asserted-by":"crossref","unstructured":"Piskac, R. and Kuncak, V. 2008. Decision procedures for multisets with cardinality constraints. In Verification, Model Checking, and Abstract Interpretation, 9th International Conference, VMCAI 2008, San Francisco, USA, January 7\u20139, 2008, Proceedings, Logozzo, F. , Peled, D. A. , and Zuck, L. D. , Eds. Lecture Notes in Computer Science, vol. 4905. Springer, 218\u2013232.","DOI":"10.1007\/978-3-540-78163-9_20"},{"key":"S1471068421000521_ref37","unstructured":"Rossi, G. 2008. $$\\{ log\\} $$ . http:\/\/people.dmi.unipr.it\/gianfranco.rossi\/setlog.Home.html. Last access 2021."},{"key":"S1471068421000521_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09577-6"},{"key":"S1471068421000521_ref39","unstructured":"Spivey, J. M. 1992. The Z Notation: A Reference Manual. Prentice Hall International (UK) Ltd., Hertfordshire, UK, UK."},{"key":"S1471068421000521_ref41","unstructured":"Stump, A. , Barrett, C. W. , Dill, D. L. and Levitt, J. R. 2001. A decision procedure for an extensional theory of arrays. In 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings. IEEE Computer Society, 29\u201337."},{"key":"S1471068421000521_ref45","doi-asserted-by":"crossref","unstructured":"Zarba, C. G. 2002a. Combining multisets with integers. In Automated Deduction - CADE-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings, Voronkov, A , Ed. Lecture Notes in Computer Science, vol. 2392. Springer, 363\u2013376.","DOI":"10.1007\/3-540-45620-1_30"},{"key":"S1471068421000521_ref5","doi-asserted-by":"crossref","unstructured":"Bender, M. and Sofronie-Stokkermans, V. 2017. Decision procedures for theories of sets with measures. In Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, de Moura, L. , Ed. Lecture Notes in Computer Science, vol. 10395. Springer, 166\u2013184.","DOI":"10.1007\/978-3-319-63046-5_11"},{"volume-title":"Monographs in Computer Science","year":"2001","author":"Cantone","key":"S1471068421000521_ref8"}],"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\/S1471068421000521","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,2]],"date-time":"2023-04-02T23:38:23Z","timestamp":1680478703000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068421000521\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,9]]},"references-count":47,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,3]]}},"alternative-id":["S1471068421000521"],"URL":"https:\/\/doi.org\/10.1017\/s1471068421000521","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"type":"print","value":"1471-0684"},{"type":"electronic","value":"1475-3081"}],"subject":[],"published":{"date-parts":[[2021,11,9]]},"assertion":[{"value":"\u00a9 The Author(s), 2021. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}