Faster Certified Symmetry Breaking Using Orders with Auxiliary Variables

Symmetry breaking is a crucial technique in modern combinatorial 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 solution, but also a mathematical proof of correctness in a standard 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 remained a long-standing open challenge. A fully general approach was recently proposed, 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 symmetry breaking using the state-of-the-art satsuma symmetry breaker and the VeriPB proof checking toolchain.

Authors

• Markus Anders RPTU Kaiserslautern-Landau, Kaiserslautern, Germany
• Bart Bogaerts KU Leuven, Belgium Vrije Universiteit Brussel, Belgium
• Benjamin Bogø University of Copenhagen, Copenhagen, Denmark Lund University, Lund, Sweden
• Arthur Gontier University of Glasgow, Glasgow, Scotland
• Wietze Koops Lund University, Lund, Sweden University of Copenhagen, Copenhagen, Denmark
• Ciaran McCreesh University of Glasgow, Scotland (UK)
• Magnus O. Myreen Chalmers University of Technology, Gothenburg, Sweden
• Jakob Nordström University of Copenhagen, Copenhagen, Denmark Lund University, Lund, Sweden
• Andy Oertel Lund University, Lund, Sweden University of Copenhagen, Copenhagen, Denmark
• Adrian Rebola-Pardo Vienna University of Technology, Vienna, Austria Johannes Kepler University Linz, Linz, Austria
• Yong Kiam Tan Institute for Infocomm Research (I2R), A*STAR, Singapore

Keywords

No keywords are indexed for this paper.