Certified SAT Covering-Radius Measurement: Representation Invariance and Lazy-Constraint Experiments

This technical note studies how reliably and efficiently one can measure the geometric coverage of recorded solutions to a Boolean satisfiability problem. The observable is the solution-relative covering radius: the greatest Hamming distance from any satisfying assignment to its nearest recorded solution. The first part establishes representation invariance when distances are measured on the original variables, provided both the solution set and the recorded sample project correctly. Including auxiliary variables can increase the covering radius by at most their number. This classical covering-radius inequality is presented in a solution-relative setting, together with a comparison-margin criterion distinguishing orderings guaranteed to survive re-encoding from those for which that guarantee is unavailable. The second part evaluates two implementation changes using independently verified witnesses and clausal refutations. Tightening lower bounds to witnesses’ actual distances improves none of the final bounds across 257 reconstructed measurements. A nine-unit experiment on 64-variable instances finds mixed results for lazy distance-constraint generation: it reduces measurement time on completed cases, principally through cheaper proof checking, but produces wider certified intervals on four of five unresolved cases under the fixed budget.