Faster Certified Symmetry Breaking Using Orders With Auxiliary Variables

TL;DR

The paper tackles the challenge of certifying symmetry-breaking reasoning in SAT solvers, where prior approaches encoded lexicographic orders with large integer coefficients, hindering proof logging and checking for large symmetries. It introduces encoding orders with auxiliary variables and a redesigned VeriPB-based proof system that uses a specification over these auxiliaries to maintain implicational proofs, enabling dominance- and redundance-based strengthening to certify symmetry-breaking constraints. The authors demonstrate asymptotic improvements (at least a linear factor in the order size $n$) and validate the approach through an end-to-end, formally verified toolchain comprising satsuma for generation and VeriPB/CakePB for checking. Experimental results show orders-of-magnitude improvements in proof logging and checking, with the new method outperforming the previous approach on crafted benchmarks and real SAT competition data, while incurring only modest overhead. This work considerably enhances the practicality of certified symmetry breaking for large-scale problems, paving the way for dynamic and conditional symmetry techniques in the future.

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 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 symmetry breaking using the state-of-the-art satsuma symmetry breaker and the VeriPB proof checking toolchain.

Figures (2)

• Figure 1: On top, the cost of running satsuma with or without proof logging, on crafted benchmark instances, as the instance size grows. In each case logging with the new method scales similarly to not doing logging, whilst the old method exhibits worse scaling for several families. On the bottom, the cost of checking these proofs: the new method exhibits better scaling.
• Figure 2: On the left, the cumulative number of "interesting" SAT competition instances broken, logged, and checked over time. The centre plot compares the added cost of writing proofs with the old and new methods, compared to not writing proofs; 52 instances reached time or memory limits with the old method. The right-hand plot compares the cost of checking proofs using the old and new methods, with points below the diagonal line showing where both methods succeeded but the new method was faster; additionally, 8 and 30 instances reach limits with VeriPB and CakePB respectively with the new method where the old method succeeded, compared to 95 and 97 respectively with the old method where the new method succeeded.

Theorems & Definitions (44)

• Definition 1
• Lemma 1
• Definition 2
• Lemma 2
• Definition 3
• Lemma 3
• Definition 4: Dominance-based strengthening with specification
• Lemma 4
• Definition 5: Redundance-based strengthening with specification
• Lemma 5