{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T09:08:57Z","timestamp":1743152937119,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031308192"},{"type":"electronic","value":"9783031308208"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T00:00:00Z","timestamp":1681948800000},"content-version":"vor","delay-in-days":109,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Constraint programming systems allow a diverse range of problems to be modelled and solved. Most systems require the user to learn a new constraint programming language, which presents a barrier to novice and casual users. To address this problem, we present the CoPTIC constraint programming system, which allows the user to write a model in the well-known programming language C, augmented with a simple API to support using a <jats:italic>guess-and-check<\/jats:italic> paradigm. The resulting model is at most as complex as an ordinary C program that uses naive brute force to solve the same problem.<\/jats:p><jats:p>CoPTIC uses the bounded model checker CBMC to translate the model into a SAT instance, which is solved using the SAT solver CaDiCaL. We show that, while this is less efficient than a direct translation from a dedicated constraint language into SAT, performance remains adequate for casual users. CoPTIC supports constraint satisfaction and optimisation problems, as well as enumeration of multiple solutions. After a solution has been found, CoPTIC allows the model to be run with the solution; this makes it easy to debug a model, or to print the solution in any desired format.<\/jats:p>","DOI":"10.1007\/978-3-031-30820-8_13","type":"book-chapter","created":{"date-parts":[[2023,4,19]],"date-time":"2023-04-19T19:02:36Z","timestamp":1681930956000},"page":"173-191","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["CoPTIC: Constraint Programming Translated Into C"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2323-1771","authenticated-orcid":false,"given":"Martin Mariusz","family":"Lester","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,4,20]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","unstructured":"Audemard, G., Boussemart, F., Lecoutre, C., Piette, C., Roussel, O.: Xcsp$${}^{\\text{3}}$$ and its ecosystem. Constraints An Int. J. 25(1-2), 47\u201369 (2020). https:\/\/doi.org\/10.1007\/s10601-019-09307-9, https:\/\/doi.org\/10.1007\/s10601-019-09307-9","DOI":"10.1007\/s10601-019-09307-9"},{"key":"13_CR2","doi-asserted-by":"publisher","unstructured":"Audemard, G., Lecoutre, C., Lonca, E.: Proceedings of the 2022 XCSP3 competition. CoRR abs\/2209.00917 (2022). https:\/\/doi.org\/10.48550\/arXiv.2209.00917, https:\/\/doi.org\/10.48550\/arXiv.2209.00917","DOI":"10.48550\/arXiv.2209.00917"},{"key":"13_CR3","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Lemberger, T., Tautschnig, M.: Tests from witnesses - execution-based validation of verification results. In: Dubois, C., Wolff, B. (eds.) Tests and Proofs - 12th International Conference, TAP@STAF 2018, Toulouse, France, June 27-29, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10889, pp. 3\u201323. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-92994-1_1, https:\/\/doi.org\/10.1007\/978-3-319-92994-1_1","DOI":"10.1007\/978-3-319-92994-1_1"},{"key":"13_CR4","unstructured":"Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In: Balyo, T., Froleyks, N., Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proc.\u00a0of SAT Competition 2020 \u2013 Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2020-1, pp. 51\u201353. University of Helsinki (2020), https:\/\/helda.helsinki.fi\/handle\/10138\/318450"},{"key":"13_CR5","doi-asserted-by":"publisher","unstructured":"Brodsky, A., Nash, H.: Cojava: Optimization modeling by nondeterministic simulation. In: Benhamou, F. (ed.) Principles and Practice of Constraint Programming - CP 2006, 12th International Conference, CP 2006, Nantes, France, September 25-29, 2006, Proceedings. Lecture Notes in Computer Science, vol.\u00a04204, pp. 91\u2013106. Springer (2006). https:\/\/doi.org\/10.1007\/11889205_9, https:\/\/doi.org\/10.1007\/11889205_9","DOI":"10.1007\/11889205_9"},{"key":"13_CR6","doi-asserted-by":"publisher","unstructured":"Cipriano, R., Dovier, A., Mauro, J.: Compiling and executing declarative modeling languages to gecode. In: de\u00a0la Banda, M.G., Pontelli, E. (eds.) Logic Programming, 24th International Conference, ICLP 2008, Udine, Italy, December 9-13 2008, Proceedings. Lecture Notes in Computer Science, vol.\u00a05366, pp. 744\u2013748. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-89982-2_69, https:\/\/doi.org\/10.1007\/978-3-540-89982-2_69","DOI":"10.1007\/978-3-540-89982-2_69"},{"key":"13_CR7","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings. Lecture Notes in Computer Science, vol.\u00a02988, pp. 168\u2013176. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15, https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"13_CR8","doi-asserted-by":"publisher","unstructured":"Cordeiro, L.C., Fischer, B., Marques-Silva, J.: Smt-based bounded model checking for embedded ANSI-C software. IEEE Trans. Software Eng. 38(4), 957\u2013974 (2012). https:\/\/doi.org\/10.1109\/TSE.2011.59, https:\/\/doi.org\/10.1109\/TSE.2011.59","DOI":"10.1109\/TSE.2011.59"},{"key":"13_CR9","doi-asserted-by":"publisher","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible sat-solver. In: Giunchiglia, E., Tacchella, A. (eds.) Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers. Lecture Notes in Computer Science, vol.\u00a02919, pp. 502\u2013518. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37, https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"13_CR10","doi-asserted-by":"publisher","unstructured":"Francis, K., Brand, S., Stuckey, P.J.: Optimisation modelling for software developers. In: Milano, M. (ed.) Principles and Practice of Constraint Programming - 18th International Conference, CP 2012, Qu\u00e9bec City, QC, Canada, October 8-12, 2012. Proceedings. Lecture Notes in Computer Science, vol.\u00a07514, pp. 274\u2013289. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-33558-7_22, https:\/\/doi.org\/10.1007\/978-3-642-33558-7_22","DOI":"10.1007\/978-3-642-33558-7_22"},{"key":"13_CR11","unstructured":"Frisch, A.M., Grum, M., Jefferson, C., Hern\u00e1ndez, B.M., Miguel, I.: The design of ESSENCE: A constraint language for specifying combinatorial problems. In: Veloso, M.M. (ed.) IJCAI 2007, Proceedings of the 20th International Joint Conference on Artificial Intelligence, Hyderabad, India, January 6-12, 2007. pp. 80\u201387 (2007), http:\/\/ijcai.org\/Proceedings\/07\/Papers\/011.pdf"},{"key":"13_CR12","doi-asserted-by":"publisher","unstructured":"Gent, I.P., Walsh, T.: Csp$${}_{\\text{lib }}$$: A benchmark library for constraints. In: Jaffar, J. (ed.) Principles and Practice of Constraint Programming - CP\u201999, 5th International Conference, Alexandria, Virginia, USA, October 11-14, 1999, Proceedings. Lecture Notes in Computer Science, vol.\u00a01713, pp. 480\u2013481. Springer (1999). https:\/\/doi.org\/10.1007\/978-3-540-48085-3_36, https:\/\/doi.org\/10.1007\/978-3-540-48085-3_36","DOI":"10.1007\/978-3-540-48085-3_36"},{"key":"13_CR13","unstructured":"Gent, I.P., Walsh, T.: Csplib: Twenty years on. CoRR abs\/1909.13430 (2019), http:\/\/arxiv.org\/abs\/1909.13430"},{"key":"13_CR14","unstructured":"Lester, M.M.: Solving interactive fiction games via partial evaluation and bounded model checking. CoRR abs\/2012.15365 (2020), https:\/\/arxiv.org\/abs\/2012.15365"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Lester, M.M.: CoPTIC: Constraint programming translated into C (Nov 2022). https:\/\/doi.org\/10.5281\/zenodo.7313351, https:\/\/doi.org\/10.5281\/zenodo.7313351","DOI":"10.5281\/zenodo.7313351"},{"key":"13_CR16","unstructured":"Manthey, N.: Solving summle.net with SAT. In: Balyo, T., Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proc.\u00a0of SAT Competition 2022 \u2013 Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2022-1, pp. 70\u201371. University of Helsinki (2022), http:\/\/hdl.handle.net\/10138\/318450"},{"key":"13_CR17","doi-asserted-by":"publisher","unstructured":"Nethercote, N., Stuckey, P.J., Becket, R., Brand, S., Duck, G.J., Tack, G.: Minizinc: Towards a standard CP modelling language. In: Bessiere, C. (ed.) Principles and Practice of Constraint Programming - CP 2007, 13th International Conference, CP 2007, Providence, RI, USA, September 23-27, 2007, Proceedings. Lecture Notes in Computer Science, vol.\u00a04741, pp. 529\u2013543. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-74970-7_38, https:\/\/doi.org\/10.1007\/978-3-540-74970-7_38","DOI":"10.1007\/978-3-540-74970-7_38"},{"key":"13_CR18","doi-asserted-by":"publisher","unstructured":"Rakamaric, Z., Emmi, M.: SMACK: decoupling source language details from verifier implementations. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. Lecture Notes in Computer Science, vol.\u00a08559, pp. 106\u2013113. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_7, https:\/\/doi.org\/10.1007\/978-3-319-08867-9_7","DOI":"10.1007\/978-3-319-08867-9_7"},{"key":"13_CR19","doi-asserted-by":"publisher","unstructured":"Triska, M., Musliu, N.: An improved SAT formulation for the social golfer problem. Ann. Oper. Res. 194(1), 427\u2013438 (2012). https:\/\/doi.org\/10.1007\/s10479-010-0702-5, https:\/\/doi.org\/10.1007\/s10479-010-0702-5","DOI":"10.1007\/s10479-010-0702-5"},{"key":"13_CR20","doi-asserted-by":"publisher","unstructured":"Verma, S., Yap, R.H.C.: Benchmarking symbolic execution using constraint problems - initial results. In: 31st IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2019, Portland, OR, USA, November 4-6, 2019. pp.\u00a01\u20139. IEEE (2019). https:\/\/doi.org\/10.1109\/ICTAI.2019.00010, https:\/\/doi.org\/10.1109\/ICTAI.2019.00010","DOI":"10.1109\/ICTAI.2019.00010"},{"key":"13_CR21","doi-asserted-by":"publisher","unstructured":"Zhou, N.: In pursuit of an efficient SAT encoding for the hamiltonian cycle problem. In: Simonis, H. (ed.) Principles and Practice of Constraint Programming - 26th International Conference, CP 2020, Louvain-la-Neuve, Belgium, September 7-11, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12333, pp. 585\u2013602. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-58475-7_34, https:\/\/doi.org\/10.1007\/978-3-030-58475-7_34","DOI":"10.1007\/978-3-030-58475-7_34"},{"key":"13_CR22","doi-asserted-by":"publisher","unstructured":"Zhou, N., Kjellerstrand, H.: The picat-sat compiler. In: Gavanelli, M., Reppy, J.H. (eds.) Practical Aspects of Declarative Languages - 18th International Symposium, PADL 2016, St. Petersburg, FL, USA, January 18-19, 2016. Proceedings. Lecture Notes in Computer Science, vol.\u00a09585, pp. 48\u201362. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-28228-2_4, https:\/\/doi.org\/10.1007\/978-3-319-28228-2_4","DOI":"10.1007\/978-3-319-28228-2_4"},{"key":"13_CR23","doi-asserted-by":"publisher","unstructured":"Zhou, N., Kjellerstrand, H.: Optimizing SAT encodings for arithmetic constraints. In: Beck, J.C. (ed.) Principles and Practice of Constraint Programming - 23rd International Conference, CP 2017, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10416, pp. 671\u2013686. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-66158-2_43, https:\/\/doi.org\/10.1007\/978-3-319-66158-2_43","DOI":"10.1007\/978-3-319-66158-2_43"},{"key":"13_CR24","doi-asserted-by":"publisher","unstructured":"Zhou, N., Kjellerstrand, H., Fruhman, J.: Constraint Solving and Planning with Picat. Springer Briefs in Intelligent Systems, Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-25883-6, https:\/\/doi.org\/10.1007\/978-3-319-25883-6","DOI":"10.1007\/978-3-319-25883-6"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30820-8_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,2]],"date-time":"2023-08-02T11:04:05Z","timestamp":1690974245000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30820-8_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308192","9783031308208"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30820-8_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"20 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"169","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"56","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}