Faster Certified Symmetry Breaking Using Orders With Auxiliary Variables

Symmetry breaking is a crucial technique in modern combi-
natorial solving, but it is difficult to be sure it is implemented
correctly. The most successful approach to deal with bugs is
to make solvers certifying, so that they output not just a so-
lution, but also a mathematical proof of correctness in a stan-
dard format, which can then be checked by a formally verified
checker. This requires justifying symmetry reasoning within
the proof, but developing efficient methods for this has re-
mained a long-standing open challenge. A fully general ap-
proach was recently proposed by Bogaerts et al. (2023), but
it relies on encoding lexicographic orders with big integers,
which quickly becomes infeasible for large symmetries. In
this work, we develop a method for instead encoding orders
with auxiliary variables. We show that this leads to orders-of-
magnitude speed-ups in both theory and practice by running
experiments on proof logging and checking for SAT symme-
try breaking using the state-of-the-art SATSUMA symmetry
breaker and the V ERIPB proof checking toolchain.