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

NOBLECOUNT FOR LOCAL SEARCH IN SAT — FLOC’2026

1

Background: SAT & Local Search

NOBLECOUNT FOR LOCAL SEARCH IN SAT — FLOC’2026

2

[1] Fu et al. (2024), “Improving Two-Mode Algorithm via Probabilistic Selection for SAT.”

[2] Biere et al. (2024), “CaDiCaL 2.0.”

How Local Search Works

• LS maintains a complete assignment (every variable has a value)
• Core operation: the flip — select a variable, invert its assignment
• Two per-variable scores guide flip selection:
• make(x): # unsatisfied clauses that become satisfied if x is flipped
• break(x): # satisfied clauses that become unsatisfied if x is flipped
• score(x) = make(x) - break(x)
• After each flip, make and break must be updated for all affected variables

NOBLECOUNT FOR LOCAL SEARCH IN SAT — FLOC’2026

3

Local Search Performance

• Flips/sec is our key performance metric
• Each flip touches many clauses, and clause database access is costly
• Goal: minimize clause accesses per flip
• Known optimizations already reduce this access

This work:

• NobleCount: a forgotten scheme that cuts accesses and boosts performance
• Integrating NobleCount to the leading LS solver - ProbCCanr
• Potential reaches beyond this work (work in progress)

NOBLECOUNT FOR LOCAL SEARCH IN SAT — FLOC’2026

4

Local Search – Reducing Clause Access

Additional compact data structure that is faster to access:

• Per-clause Satisfied Literal Count (SLC): # of true literals in clause
• When variable x is flipped, the SLC of each clause changes by ±1
• We reduce access to the clause database by accessing SLC

​

​

NOBLECOUNT FOR LOCAL SEARCH IN SAT — FLOC’2026

5

SLC

Clause-State Transitions

• 6 transition types (3 for SLC increase, 3 for decrease):
• SLC > 2: no score updates, no clause access — essentially free
• 0→1, 1→0: clause crosses SAT/UnSAT boundary → clause access
• 1→2, 2→1: only the critical variable's break must be updated
• Fukunaga (2004): 1→2 + 2→1 together = 57%–82% of all clause-state changes

​

We want to reduce clause access for the 1→2 + 2→1 transitions!

NOBLECOUNT FOR LOCAL SEARCH IN SAT — FLOC’2026

6

NobleCount: The Core Idea

We keep a little extra data with every clause

• Beside the SLC, a XOR of its satisfied literals (can also be the sum)

Why it helps

• The costly step: find a clause’s lone satisfied literal
• When SLC = 1, the XOR is that literal → O(1); no clause scan!

It works by…

• Each flip: SLC ±1, XOR the literal in or out — branch-free

​

We call the new compact data-structure the Light Data

NOBLECOUNT FOR LOCAL SEARCH IN SAT — FLOC’2026

7

NOBLECOUNT FOR LOCAL SEARCH IN SAT — FLOC’2026

8

The NobleCount Scheme

NOBLECOUNT FOR LOCAL SEARCH IN SAT — FLOC’2026

9

The NobleCount Scheme

Occ. Lists

Clause DB

NOBLECOUNT FOR LOCAL SEARCH IN SAT — FLOC’2026

10

The NobleCount Scheme

Occ. Lists

Update

Clause DB

NOBLECOUNT FOR LOCAL SEARCH IN SAT — FLOC’2026

11

The NobleCount Scheme

Occ. Lists

Clause DB

Update

NOBLECOUNT FOR LOCAL SEARCH IN SAT — FLOC’2026

12

The NobleCount Scheme

Occ. Lists

Clause DB

Update

NOBLECOUNT FOR LOCAL SEARCH IN SAT — FLOC’2026

13

The NobleCount Scheme

Occ. Lists

Clause DB

Update

NobleCount: A Forgotten Optimization

• Introduced in NanoSAT (Biere, 2004) for CDCL SAT solving
• Brought to Local Search by Balint et al. (2014): probSAT & Sparrow
• Proven: over 2× speedups on hard combinatorial instances
• A simple, low-risk change: no heuristic or algorithm needs to change

​

Yet it never reached today’s strongest LS solvers !

NOBLECOUNT FOR LOCAL SEARCH IN SAT — FLOC’2026

14

A Tale of Two Lineages

NOBLECOUNT FOR LOCAL SEARCH IN SAT — FLOC’2026

15

Two lineages evolved in parallel

• TaSSAT kept NobleCount throughout probSAT
• ProbCCAnr (CCA line) never adopted it

This work:

• Add NobleCount to ProbCCAnr
• Compare against TaSSAT

Experimental Setup

• Hardware: Intel Xeon Gold 6230 @ 2.10 GHz, 32 GB memory limit
• Fixed random seed; one run per instance; max timeout 300s
• Metric: PAR2 — unsolved instances penalized at 2× timeout (lower is better)
• Three configurations:
• NC — ProbCCAnr + NobleCount
• Base — unmodified ProbCCAnr
• TS — TaSSAT
• Two benchmark families:
• FCC: 10,000 US Federal Communications Commission spectrum-repacking instances
• SC22: 5,355 instances from the SC22 anniversary track (structured + combinatorial)

NOBLECOUNT FOR LOCAL SEARCH IN SAT — FLOC’2026

16

NOBLECOUNT FOR LOCAL SEARCH IN SAT — FLOC’2026

17

−24.8% PAR2 at 20s (NC vs Base) �

FCC Benchmark Results

NOBLECOUNT FOR LOCAL SEARCH IN SAT — FLOC’2026

18

SC22 Anniversary Benchmark

Future Work & Broader Applicability

• Broader LS solver adoption
• Other LS solvers missing NobleCount
• Anytime MaxSAT solvers
• Rely on LS to improve the first solution
• Early solution quality is critical — benefits of NobleCount are immediate
• SIMD / GPU parallelism
• Branch-free, uniform update applies
• Ideal candidate for SIMD vectorization or massively parallel GPU-based execution

NOBLECOUNT FOR LOCAL SEARCH IN SAT — FLOC’2026

19

GPU parallelism - Work In Progress

NOBLECOUNT FOR LOCAL SEARCH IN SAT — FLOC’2026

20

Occ. Lists

Update

GPU parallelism - Work In Progress

NOBLECOUNT FOR LOCAL SEARCH IN SAT — FLOC’2026

21

Occ. Lists

Update

yogevshalmon@campus.technion.ac.il

NOBLECOUNT FOR LOCAL SEARCH IN SAT — FLOC’2026

22