Ciaran McCreesh

• I am 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.
• Email: ciaran.mccreesh at glasgow.ac.uk .
• Office: S122 Lilybank Gardens. Enter through the Sir Alwyn Williams building, through the glass double doors, up two and a half a flight of stairs to the floor marked S, along the corridor until you see room numbers that start with a 12, and it's on the left.

Research interests

I'm interested in solving hard combinatorial problems in practice, particularly in the areas of graph theory and subgraph finding. Theoretically, these problems should take exponential time to solve, but in practice algorithms based upon symbolic artificial intelligence techniques like constraint programming and boolean satisfiability can often exactly solve large instances very quickly. My main research questions are:

• What can we do to close the gap between theoretical worst-case results, and what we see in practice? I am particularly interested in using empirical algorithmics and computational and scientific experiments to gain an understanding that can't be reached through theory alone.
• Can we use empirical algorithmics techniques to design better algorithms? For example, can we measure what solvers are doing during search, and use this to improve performance when a solver encounters an instance it finds hard? I have also worked on exploiting parallel hardware such as bit-parallelism, multi-core parallelism and high performance computing to accelerate algorithm performance.
• Why should we trust the outputs of these algorithm implementations? Solvers are increasingly being used autonomously in ways which directly affect people's safety, lives, and livelihoods, without human oversight. However, we know that most solvers are buggy, and will occasionally output an incorrect answer. Conventional software engineering testing techniques fail to detect these bugs, and formal methods are too expensive to use in practice. Some of my recent research looks at proof logging or certifying as an alternative. The idea is that alongside an output, a solver produces a mathematical proof that this answer is correct, which can be stored and audited by a third party.
• How can we make techniques developed in constraint programming and related areas more accessible to developers? We know, for example, that vanilla backtracking search is a bad idea, but techniques like restarts and nogood recording are not widely implemented due to the difficulty in programming them correctly. Similarly, we know how to do parallel search in theory, but few algorithm implementations actually do this. Could we develop libraries or algorithm skeletons to help?
• More broadly, can we develop a discipline of algorithm engineering that focuses on how to design and implement small, efficient, correct pieces of code, rather than the large systems with uncertain requirements usually covered by software engineering?

Proof logging tutorial

You can see slides from the IJCAI 2023 edition of our proof logging tutorial, or watch a recording of an earlier, shorter version.

Source code

• My GitHub profile contains code, experimental scripts, etc to reproduce experiments in my publications.
• The Glasgow Subgraph Solver is based upon a series of papers by (subsets of) myself, Patrick Prosser, and James Trimble. This is the version of the code you should use if you're just interested in having a good solver, rather than reproducing the results in a particular paper.
• The Glasgow Constraint Solver is a new project that brings proof logging to constraint programming.

Publications and Conference Papers

• Emir Demirović, Ciaran McCreesh, Matthew J. McIlree, Jakob Nordström, Andy Oertel and Konstantin Sidorov: Pseudo-Boolean Reasoning About States and Transitions to Certify Dynamic Programming and Decision Diagram Algorithms.
  CP 2024.
  [author-final PDF, supplementary material]
• Matthew J. McIlree, Ciaran McCreesh and Jakob Nordström: Proof Logging for the Circuit Constraint.
  CPAIOR 2024.
  [author-final PDF, supplementary material]
• Stephan Gocht, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel and Yong Kiam Tan: End-to-End Verification for Subgraph Solving.
  AAAI 2024.
  [author-final PDF, supplemental material]
• Matthew J. McIlree and Ciaran McCreesh: Proof Logging for Smart Extensional Constraints.
  CP 2023. Best Paper Award.
  [DOI, author-final PDF]
• Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, Jakob Nordström: Certified Dominance and Symmetry Breaking for Combinatorial Optimisation.
  Journal of Artificial Intelligence Research (JAIR) 77: 1539-1589 (2023).
  [DOI]
• Stephan Gocht, Ciaran McCreesh and Jakob Nordström: An Auditable Constraint Programming Solver
  CP 2022.
  [DOI, author-final PDF, source code]
• Bart Bogaerts, Stephan Gocht, Ciaran McCreesh and Jakob Nordström: Certified Symmetry and Dominance Breaking for Combinatorial Optimisation.
  AAAI 2022. Distinguished Paper Award.
  [DOI, author-final PDF, longer version with appendices, supplemental material]
• Blair Archibald, Kyle Burns, Ciaran McCreesh and Michele Sevegnani: Practical Bigraphs via Subgraph Isomorphism.
  CP 2021.
  [DOI, author-final PDF]
• Johannes K. Fichte, Markus Hecher, Ciaran McCreesh and Anas Shahab: Complications for Computational Experiments from Modern Processors.
  CP 2021.
  [DOI, author-final PDF]
• Sonja Kraiczy and Ciaran McCreesh: Solving Graph Homomorphism and Subgraph Isomorphism Problems Faster Through Clique Neighbourhood Constraints.
  IJCAI 2021.
  [DOI, author-final PDF, Supplementary material]
• Özgür Akgün, Jessica Enright, Christopher Jefferson, Ciaran McCreesh, Patrick Prosser and Steffen Zschaler: Finding Subgraphs With Side Constraints.
  CPAIOR 2021.
  [DOI, author-final PDF, code]
• Stephan Gocht, Ross McBride, Ciaran McCreesh, Jakob Nordström, Patrick Prosser and James Trimble: Certifying Solvers for Clique and Maximum Common (Connected) Subgraph Problems.
  CP 2020.
  [DOI, author-final PDF]
• Ciaran McCreesh, Patrick Prosser and James Trimble: The Glasgow Subgraph Solver: Using Constraint Programming to Tackle Hard Subgraph Isomorphism Problem Variants.
  Tool paper. ICGT 2020.
  [DOI, author-final PDF]
• Stephan Gocht, Ciaran McCreesh and Jakob Nordström: Subgraph Isomorphism Meets Cutting Planes: Solving With Certified Solutions.
  IJCAI 2020.
  [DOI, author-final PDF]
• Jan Elffers, Stephan Gocht, Ciaran McCreesh and Jakob Nordström: Justifying All Differences Using Pseudo-Boolean Reasoning.
  AAAI 2020.
  [DOI, author-final PDF]
• Ciaran McCreesh, William Pettersson and Patrick Prosser: Understanding the Empirical Hardness of Random Optimisation Problem.
  CP 2019: 333-349.
  [DOI, author-final PDF]
• Blair Archibald, Fraser Dunlop, Ruth Hoffmann, Ciaran McCreesh, Patrick Prosser and James Trimble: Sequential and Parallel Solution-Biased Search for Subgraph Algorithms.
  CPAIOR 2019: 20-38.
  [DOI, author-final PDF, source code]
• Ian P. Gent, Ian Miguel, Peter Nightingale, Ciaran McCreesh, Patrick Prosser, Neil C. A. Moore, Chris Unsworth: A review of literature on parallel constraint solving.
  TPLP 18(5-6): 725-758 (2018).
  [DOI, author-final PDF]
• José Cano, David Robert White, Alejandro Bordallo, Ciaran McCreesh, Anna Lito Michala, Jeremy Singer, Vijay Nagarajan: Solving the task variant allocation problem in distributed robotics.
  Auton. Robots 42(7): 1477-1495 (2018).
  [DOI (open access)]
• Ciaran McCreesh, Patrick Prosser, Christine Solnon and James Trimble: When Subgraph Isomorphism is Really Hard, and Why This Matters for Graph Databases.
  Journal of Artificial Intelligence Research (JAIR) 61: 723-759 (2018).
  [DOI (open access), Author-final PDF]
• Ruth Hoffmann, Ciaran McCreesh, Samba Ndojh Ndiaye, Patrick Prosser, Craig Reilly, Christine Solnon, and James Trimble: Observations from Parallelising Three Maximum Common (Connected) Subgraph Algorithms.
  CPAIOR 2018: 298-315.
  [author-final PDF, source code]
• Blair Archibald, Patrick Maier, Ciaran McCreesh, Robert Stewart and Phil Trinder: Replicable parallel branch and bound search.
  Journal of Parallel and Distributed Computing, Volume 113, 92-114 (2018)
  [DOI (open access)]
• Ciaran McCreesh: Solving Hard Subgraph Problems in Parallel.
  PhD thesis. University of Glasgow, 2017.
  [PDF]
• Ciaran McCreesh, Patrick Prosser, Kyle Simpson and James Trimble: On Maximum Weight Clique Algorithms, and How They Are Evaluated.
  CP 2017: 206-225.
  [DOI, author-final PDF, maximum weight clique benchmark instances]
• Ciaran McCreesh, Patrick Prosser and James Trimble: A Partitioning Algorithm for Maximum Common Subgraph Problems.
  IJCAI 2017: 712-719.
  [DOI, author-final PDF, source code]
• Ruth Hoffmann, Ciaran McCreesh and Craig Reilly: Between Subgraph Isomorphism and Maximum Common Subgraph.
  AAAI 2017: 3907-3914.
  [abstract and PDF, author-final PDF, Source code]
• Ciaran McCreesh, Samba Ndojh Ndiaye, Patrick Prosser and Christine Solnon: Clique and Constraint Models for Maximum Common (Connected) Subgraph Problems.
  CP 2016: 350-368.
  [DOI, author-final PDF, Source code]
• Ciaran McCreesh, Patrick Prosser and James Trimble: Morphing between Stable Matching Problems
  CP 2016: 832-840
  [DOI, author-final PDF]
• Ciaran McCreesh, Patrick Prosser and James Trimble: Heuristics and Really Hard Instances for Subgraph Isomorphism Problems.
  IJCAI 2016: 631-638.
  [abstract and PDF, author-final PDF, Source code]
• Ciaran McCreesh and Patrick Prosser: Finding Maximum k-Cliques Faster Using Lazy Global Domination.
  SoCS 2016: 72-80.
  [abstract and PDF, author-final PDF, Older preprint on arXiv, Source code]
• Jose Cano Reyes, David White, Alejandro Bordallo, Ciaran McCreesh, Patrick Prosser, Jeremy Singer and Vijay Nagarajan: Task Variant Allocation in Distributed Robotics.
  Robotics Science and Systems 2016.
  [PDF, author-final PDF]
• Lars Kotthoff, Ciaran McCreesh and Christine Solnon: Portfolios of Subgraph Isomorphism Algorithms.
  LION 2016: 107-122.
  [DOI, author-final PDF, Source code]
• Ciaran McCreesh, Patrick Prosser: A Parallel, Backjumping Subgraph Isomorphism Algorithm using Supplemental Graphs.
  CP 2015: 295-312.
  [DOI, author-final PDF, code, datasets, experimental scripts, VM for recomputation]
• Craig Macdonald, Ciaran McCreesh, Alice Miller and Patrick Prosser: Constructing Sailing Match Race Schedules: Round-Robin Pairing Lists.
  CP 2015: 671-686
  [DOI, author-final PDF]
• Ciaran McCreesh, Patrick Prosser: The Shape of the Search Tree for the Maximum Clique Problem, and the Implications for Parallel Branch and Bound.
  ACM Transactions on Parallel Computing Volume 2 Issue 1 (2015).
  [DOI, Older preprint on arXiv].
• Ciaran McCreesh, Patrick Prosser: A Parallel Branch and Bound Algorithm for the Maximum Labelled Clique Problem.
  Optimization Letters (2014)
  [DOI (open access)].
• Ciaran McCreesh, Patrick Prosser: Reducing the Branching in a Branch and Bound Algorithm for the Maximum Clique Problem.
  CP 2014: 549-563
  [DOI, author-final PDF]
• Ciaran McCreesh, Patrick Prosser: An Exact Branch and Bound Algorithm with Symmetry Breaking for the Maximum Balanced Induced Biclique Problem.
  CPAIOR 2014: 226-234
  [DOI, author-final PDF]
• Ciaran McCreesh, Patrick Prosser: Multi-Threading a State-of-the-Art Maximum Clique Algorithm.
  Algorithms 6(4): 618-635 (2013)
  [DOI (open access)]