{"id":3558,"date":"2025-09-15T15:55:01","date_gmt":"2025-09-15T14:55:01","guid":{"rendered":"https:\/\/blogs.qub.ac.uk\/dipsa\/?p=3558"},"modified":"2026-05-06T20:17:27","modified_gmt":"2026-05-06T19:17:27","slug":"invited-talk-a-constraint-programming-solver-you-can-trust-but-dont-have-to-by-ciaran-mccreesh","status":"publish","type":"post","link":"https:\/\/blogs.qub.ac.uk\/dipsa\/invited-talk-a-constraint-programming-solver-you-can-trust-but-dont-have-to-by-ciaran-mccreesh\/","title":{"rendered":"Invited Talk – A Constraint Programming Solver You Can Trust (But Don’t Have To) by Ciaran McCreesh"},"content":{"rendered":"\n

28 August 2025<\/p>\n\n\n\n

Abstract<\/h2>\n\n\n\n

Constraint programming is a declarative way of solving hard combinatorial, scheduling, resource allocation, and logistics problems. We specify a problem in a high-level language, give it to a solver, and the solver thinks for a while and then gives us the optimal answer. Unfortunately, even the best commercial and academic solvers contain bugs and will occasionally give a wrong answer, potentially with devastating effects. One way of avoiding this situation is through proof logging, where solvers are modified to output a mathematical proof of correctness alongside their solution. This proof can then be independently audited by a very simple (and potentially even formally verified) proof-checking tool, giving us complete confidence in the correctness of solutions (although not the solvers themselves). I’ll explain how proof logging works in general, and give an overview of the challenges and fun involved in bringing it to constraint programming. Ultimately, the aim here is to make algorithms something people can trust with their lives and livelihoods, just as engineers have already done with bridges, planes, and lifts.<\/p>\n\n\n\n

Bio<\/h2>\n\n\n\n

Ciaran McCreesh is a Royal Academy of Engineering Research Fellow working in the Formal Analysis, Theory and Algorithms group in the School of Computing Science at the University of Glasgow. His research looks at practical parallel algorithms, particularly in relation to hard subgraph problems. His publications cover combinatorial search, parallel algorithms, and constraint programming.<\/p>\n\n\n\n

\n
\"\"<\/figure>\n\n\n\n
\"\"<\/figure>\n\n\n\n
\"\"<\/figure>\n\n\n\n
\"\"<\/figure>\n<\/figure>\n","protected":false},"excerpt":{"rendered":"

28 August 2025 Abstract Constraint programming is a declarative way of solving hard combinatorial, scheduling, resource allocation, and logistics problems. We specify a problem in a high-level language, give it to a solver, and the solver thinks for a while and then gives us the optimal answer. Unfortunately, even the best commercial and academic solvers […]<\/p>\n","protected":false},"author":974,"featured_media":0,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":""},"categories":[154],"tags":[33],"class_list":["post-3558","post","type-post","status-publish","format-standard","category-talks","tag-seminars","czr-hentry"],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/blogs.qub.ac.uk\/dipsa\/wp-json\/wp\/v2\/posts\/3558","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/blogs.qub.ac.uk\/dipsa\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/blogs.qub.ac.uk\/dipsa\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/blogs.qub.ac.uk\/dipsa\/wp-json\/wp\/v2\/users\/974"}],"replies":[{"embeddable":true,"href":"https:\/\/blogs.qub.ac.uk\/dipsa\/wp-json\/wp\/v2\/comments?post=3558"}],"version-history":[{"count":2,"href":"https:\/\/blogs.qub.ac.uk\/dipsa\/wp-json\/wp\/v2\/posts\/3558\/revisions"}],"predecessor-version":[{"id":3772,"href":"https:\/\/blogs.qub.ac.uk\/dipsa\/wp-json\/wp\/v2\/posts\/3558\/revisions\/3772"}],"wp:attachment":[{"href":"https:\/\/blogs.qub.ac.uk\/dipsa\/wp-json\/wp\/v2\/media?parent=3558"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/blogs.qub.ac.uk\/dipsa\/wp-json\/wp\/v2\/categories?post=3558"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/blogs.qub.ac.uk\/dipsa\/wp-json\/wp\/v2\/tags?post=3558"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}