Abstract
Symmetry breaking can be crucial for solving hard combinatorial search and optimisation problems, but the correctness of these techniques sometimes relies on subtle arguments. For this reason, it is desirable to produce efficient, machine-verifiable certificates that solutions have been computed correctly.
In this talk, I will present our recent work on how to achieve certified static symmetry breaking (i.e., symmetry breaking as a preprocessor), as well as some yet-unpublished work demonstrating that the same techniques also apply to dynamic symmetry breaking, where the symmetries are broken during search.