NobleCount: Revisiting a Forgotten Data Structure for Local Search in SAT

Abstract

Local Search (LS) solvers for SAT can surpass CDCL solvers on some prominent satisfiable industrial and combinatorial benchmarks. They operate by flipping variable assignments and maintaining per-variable scores incrementally to guide variable selection, so performance is largely determined by how efficiently each flip is executed. We revisit a largely forgotten data structure that reduces per-flip overhead by eliminating costly clause scans. We dub this scheme NobleCount, integrate it into the leading LS solver ProbCCAnr, and evaluate it on industrial FCC spectrum-repacking instances and the SC22 anniversary track, two standard testbeds for modern LS solvers. ProbCCAnr with NobleCount achieves new state-of-the-art results on both benchmarks. On FCC, where it already overtook not only other LS solvers but also leading CDCL solvers, employing NobleCount further reduces PAR2 by 24.8% at a 20s timeout, with consistent PAR2 gains across all timeouts up to our final 300s timeout. On SC22, at longer timeouts where another LS solver, TaSSAT, originally overtakes ProbCCAnr, NobleCount lifts ProbCCAnr to outscore TaSSAT