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 sy​mmetries are broken during search.

Video Recording