{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:21:20Z","timestamp":1747592480084,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031606014"},{"type":"electronic","value":"9783031605994"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-60599-4_3","type":"book-chapter","created":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T09:02:09Z","timestamp":1716800529000},"page":"38-55","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Proof Logging for\u00a0the\u00a0Circuit Constraint"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-5042-0876","authenticated-orcid":false,"given":"Matthew J.","family":"McIlree","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6106-4871","authenticated-orcid":false,"given":"Ciaran","family":"McCreesh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2700-4285","authenticated-orcid":false,"given":"Jakob","family":"Nordstr\u00f6m","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,5,25]]},"reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-031-38499-8_1","volume-title":"Automated Deduction \u2013 CADE 29","author":"J Berg","year":"2023","unstructured":"Berg, J., Bogaerts, B., Nordstr\u00f6m, J., Oertel, A., Vandesande, D.: Certified core-guided MaxSAT solving. In: Pientka, B., Tinelli, C. (eds.) CADE 2023. LNCS, vol. 14132, pp. 1\u201322. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_1"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Bogaerts, B., Gocht, S., McCreesh, C., Nordstr\u00f6m, J.: Certified symmetry and dominance breaking for combinatorial optimisation. J. Artif. Intell. Res. 77, 1539\u20131589 (2023). Preliminary version in AAAI\u00a02022","DOI":"10.1613\/jair.1.14296"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Buss, S.R., Nordstr\u00f6m, J.: Proof complexity and SAT solving. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336, chap.\u00a07, 2nd edn., pp. 233\u2013350. IOS Press (2021)","DOI":"10.3233\/FAIA200990"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Caseau, Y., Laburthe, F.: Solving small TSPs with constraints. In: Naish, L. (ed.) Logic Programming, Proceedings of the Fourteenth International Conference on Logic Programming, Leuven, Belgium, 8\u201311 July 1997, pp. 316\u2013330. MIT Press (1997)","DOI":"10.7551\/mitpress\/4299.003.0028"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-319-59250-3_13","volume-title":"Integer Programming and Combinatorial Optimization","author":"KKH Cheung","year":"2017","unstructured":"Cheung, K.K.H., Gleixner, A., Steffy, D.E.: Verifying integer programming results. In: Eisenbrand, F., Koenemann, J. (eds.) IPCO 2017. LNCS, vol. 10328, pp. 148\u2013160. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-59250-3_13"},{"key":"3_CR6","unstructured":"Chu, G., Stuckey, P.J., Schutt, A., Ehlers, T., Gange, G., Francis, K.: Chuffed, a lazy clause generation solver (2023). https:\/\/github.com\/chuffed\/chuffed"},{"key":"3_CR7","doi-asserted-by":"publisher","unstructured":"Cook, W., Coullard, C.R., Tur\u00e1n, Gy.: On the complexity of cutting-plane proofs. Discrete Appl. Math. 18(1), 25\u201338 (1987). https:\/\/doi.org\/10.1016\/0166-218X(87)90039-4","DOI":"10.1016\/0166-218X(87)90039-4"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-319-63046-5_14","volume-title":"Automated Deduction \u2013 CADE 26","author":"L Cruz-Filipe","year":"2017","unstructured":"Cruz-Filipe, L., Heule, M.J.H., Hunt, W.A., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 220\u2013236. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_14"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-07644-7_1","volume-title":"Hybrid Metaheuristics","author":"L Di Gaspero","year":"2014","unstructured":"Di Gaspero, L., Urli, T.: A CP\/LNS approach for multi-day homecare scheduling problems. In: Blesa, M.J., Blum, C., Vo\u00df, S. (eds.) HM 2014. LNCS, vol. 8457, pp. 1\u201315. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-07644-7_1"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Elffers, J., Gocht, S., McCreesh, C., Nordstr\u00f6m, J.: Justifying all differences using pseudo-boolean reasoning. 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, 7\u201312 February 2020, pp. 1486\u20131494. AAAI Press (2020)","DOI":"10.1609\/aaai.v34i02.5507"},{"key":"3_CR11","doi-asserted-by":"publisher","unstructured":"Fages, J.G., Lorca, X.: Improving the asymmetric TSP by considering graph structure (2012). https:\/\/doi.org\/10.48550\/arXiv.1206.3437","DOI":"10.48550\/arXiv.1206.3437"},{"issue":"1","key":"3_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10601-013-9148-0","volume":"19","author":"KG Francis","year":"2014","unstructured":"Francis, K.G., Stuckey, P.J.: Explaining circuit propagation. Constraints 19(1), 1\u201329 (2014). https:\/\/doi.org\/10.1007\/s10601-013-9148-0","journal-title":"Constraints"},{"issue":"2","key":"3_CR13","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/s10601-015-9182-1","volume":"21","author":"LD Gaspero","year":"2016","unstructured":"Gaspero, L.D., Rendl, A., Urli, T.: Balancing bike sharing systems with constraint programming. Constraints 21(2), 318\u2013348 (2016). https:\/\/doi.org\/10.1007\/s10601-015-9182-1","journal-title":"Constraints"},{"key":"3_CR14","unstructured":"Gecode Team: Gecode: generic constraint development environment (2023). http:\/\/www.gecode.org"},{"key":"3_CR15","unstructured":"Gocht, S.: Certifying correctness for combinatorial algorithms: by using pseudo-Boolean reasoning. Ph.D. thesis, Lund University, Sweden (2022)"},{"key":"3_CR16","doi-asserted-by":"publisher","unstructured":"Gocht, S., McCreesh, C., Nordstr\u00f6m, J.: An auditable constraint programming solver. In: Solnon, C. (ed.) Proceeding of the 28th International Conference on Principles and Practice of Constraint Programming. Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0235, pp. 25:1\u201325:18. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2022). https:\/\/doi.org\/10.4230\/LIPIcs.CP.2022.25","DOI":"10.4230\/LIPIcs.CP.2022.25"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-030-80223-3_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2021","author":"MJH Heule","year":"2021","unstructured":"Heule, M.J.H.: Chinese remainder encoding for Hamiltonian cycles. In: Li, C.-M., Many\u00e0, F. (eds.) SAT 2021. LNCS, vol. 12831, pp. 216\u2013224. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-80223-3_15"},{"key":"3_CR18","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1016\/j.tcs.2011.11.011","volume":"447","author":"GF Italiano","year":"2012","unstructured":"Italiano, G.F., Laura, L., Santaroni, F.: Finding strong bridges and strong articulation points in linear time. Theoret. Comput. Sci. 447, 74\u201384 (2012). https:\/\/doi.org\/10.1016\/j.tcs.2011.11.011","journal-title":"Theoret. Comput. Sci."},{"key":"3_CR19","series-title":"The IBM Research Symposia Series","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-1-4684-2001-2_9","volume-title":"Complexity of Computer Computations","author":"RM Karp","year":"1972","unstructured":"Karp, R.M.: Reducibility among combinatorial problems. In: Miller, R.E., Thatcher, J.W., Bohlinger, J.D. (eds.) Complexity of Computer Computations. The IBM Research Symposia Series, pp. 85\u2013103. Springer, Boston (1972). https:\/\/doi.org\/10.1007\/978-1-4684-2001-2_9"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Kraiczy, S., McCreesh, C.: Solving graph homomorphism and subgraph isomorphism problems faster through clique neighbourhood constraints. In: Zhou, Z. (ed.) Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event\/Montreal, Canada, 19\u201327 August 2021, pp. 1396\u20131402. ijcai.org (2021). https:\/\/doi.org\/10.24963\/IJCAI.2021\/193","DOI":"10.24963\/IJCAI.2021\/193"},{"key":"3_CR21","unstructured":"Kuchcinski, K., Szymanek, R.: JaCoP - Java constraint programming solver. In: CP Solvers: Modeling, Applications, Integration, and Standardization, Co-located with the 19th International Conference on Principles and Practice of Constraint Programming (2013)"},{"issue":"3","key":"3_CR22","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/s10601-016-9241-2","volume":"21","author":"E Lam","year":"2016","unstructured":"Lam, E., Van Hentenryck, P.: A branch-and-price-and-check model for the vehicle routing problem with location congestion. Constraints 21(3), 394\u2013412 (2016). https:\/\/doi.org\/10.1007\/s10601-016-9241-2","journal-title":"Constraints"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"654","DOI":"10.1007\/978-3-319-23219-5_45","volume-title":"Principles and Practice of Constraint Programming","author":"E Lam","year":"2015","unstructured":"Lam, E., Van Hentenryck, P., Kilby, P.: Joint vehicle and crew routing and scheduling. In: Pesant, G. (ed.) CP 2015. LNCS, vol. 9255, pp. 654\u2013670. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23219-5_45"},{"key":"3_CR24","unstructured":"McCreesh, C., McIlree, M.: The Glasgow constraint solver. GitHub repository (2023). https:\/\/github.com\/ciaranm\/glasgow-constraint-solver"},{"key":"3_CR25","doi-asserted-by":"publisher","unstructured":"McIlree, M.J., McCreesh, C.: Proof logging for smart extensional constraints. In: Yap, R.H.C. (ed.) 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0280, pp. 26:1\u201326:17. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2023). https:\/\/doi.org\/10.4230\/LIPIcs.CP.2023.26","DOI":"10.4230\/LIPIcs.CP.2023.26"},{"issue":"1","key":"3_CR26","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/s12532-020-00190-7","volume":"13","author":"LD Michel","year":"2021","unstructured":"Michel, L.D., Schaus, P., Van Hentenryck, P.: MiniCP: a lightweight solver for constraint programming. Math. Program. Comput. 13(1), 133\u2013184 (2021). https:\/\/doi.org\/10.1007\/s12532-020-00190-7","journal-title":"Math. Program. Comput."},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"544","DOI":"10.1007\/978-3-540-74970-7_39","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"O Ohrimenko","year":"2007","unstructured":"Ohrimenko, O., Stuckey, P.J., Codish, M.: Propagation = lazy clause generation. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 544\u2013558. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74970-7_39"},{"key":"3_CR28","unstructured":"Perron, L., Didier, F.: CP-SAT. https:\/\/developers.google.com\/optimization\/cp\/cp_solver\/"},{"issue":"1","key":"3_CR29","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1287\/trsc.32.1.12","volume":"32","author":"G Pesant","year":"1998","unstructured":"Pesant, G., Gendreau, M., Potvin, J.Y., Rousseau, J.M.: An exact constraint logic programming algorithm for the traveling salesman problem with time windows. Transp. Sci. 32(1), 12\u201329 (1998). https:\/\/doi.org\/10.1287\/trsc.32.1.12","journal-title":"Transp. Sci."},{"key":"3_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"723","DOI":"10.1007\/978-3-642-04244-7_56","volume-title":"Principles and Practice of Constraint Programming - CP 2009","author":"C Schulte","year":"2009","unstructured":"Schulte, C., Tack, G.: Weakly monotonic propagators. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 723\u2013730. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04244-7_56"},{"issue":"2","key":"3_CR31","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R Tarjan","year":"1972","unstructured":"Tarjan, R.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146\u2013160 (1972). https:\/\/doi.org\/10.1137\/0201010","journal-title":"SIAM J. Comput."},{"key":"3_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-319-09284-3_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"N Wetzler","year":"2014","unstructured":"Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422\u2013429. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_31"},{"key":"3_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-030-58475-7_34","volume-title":"Principles and Practice of Constraint Programming","author":"N-F Zhou","year":"2020","unstructured":"Zhou, N.-F.: In pursuit of an efficient SAT encoding for the Hamiltonian cycle problem. In: Simonis, H. (ed.) CP 2020. LNCS, vol. 12333, pp. 585\u2013602. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58475-7_34"}],"container-title":["Lecture Notes in Computer Science","Integration of Constraint Programming, Artificial Intelligence, and Operations Research"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-60599-4_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T09:02:32Z","timestamp":1716800552000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-60599-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031606014","9783031605994"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-60599-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"25 May 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CPAIOR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 May 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 May 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cpaior2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sites.google.com\/view\/cpaior2024","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}