Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Faster Certified Symmetry Breaking Using Orders With Auxiliary Variables

Anders, Markus ; Bogaerts, Bart ; Bogø, Benjamin ; Gontier, Arthur ; Koops, Wietze LU orcid ; McCreesh, Ciaran ; Myreen, Magnus O. ; Nordström, Jakob LU ; Oertel, Andy LU orcid and Rebola-Pardo, Adrian , et al. (2026) 40th AAAI Conference on Artificial Intelligence, AAAI 2026 p.14140-14148
Abstract

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... (More)

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.

(Less)
Please use this url to cite or link to this publication:
author
; ; ; ; ; ; ; ; and , et al. (More)
; ; ; ; ; ; ; ; ; and (Less)
organization
publishing date
type
Chapter in Book/Report/Conference proceeding
publication status
published
subject
host publication
Proceedings of the AAAI Conference on Artificial Intelligence
editor
Koenig, Sven ; Jenkins, Chad and Taylor, Matthew E.
pages
9 pages
publisher
The Association for the Advancement of Artificial Intelligence
conference name
40th AAAI Conference on Artificial Intelligence, AAAI 2026
conference location
Singapore, Singapore
conference dates
2026-01-20 - 2026-01-27
external identifiers
  • scopus:105034610514
ISBN
9781577359067
DOI
10.1609/aaai.v40i17.38426
language
English
LU publication?
yes
id
d9c4dc4f-ebd9-4f4f-b3b3-b52327dd4d31
date added to LUP
2026-05-19 11:44:01
date last changed
2026-05-19 11:44:46
@inproceedings{d9c4dc4f-ebd9-4f4f-b3b3-b52327dd4d31,
  abstract     = {{<p>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.</p>}},
  author       = {{Anders, Markus and Bogaerts, Bart and Bogø, Benjamin and Gontier, Arthur and Koops, Wietze and McCreesh, Ciaran and Myreen, Magnus O. and Nordström, Jakob and Oertel, Andy and Rebola-Pardo, Adrian and Tan, Yong Kiam}},
  booktitle    = {{Proceedings of the AAAI Conference on Artificial Intelligence}},
  editor       = {{Koenig, Sven and Jenkins, Chad and Taylor, Matthew E.}},
  isbn         = {{9781577359067}},
  language     = {{eng}},
  pages        = {{14140--14148}},
  publisher    = {{The Association for the Advancement of Artificial Intelligence}},
  title        = {{Faster Certified Symmetry Breaking Using Orders With Auxiliary Variables}},
  url          = {{http://dx.doi.org/10.1609/aaai.v40i17.38426}},
  doi          = {{10.1609/aaai.v40i17.38426}},
  year         = {{2026}},
}