Research Direction: Restart-Aware Reward Consistency in CDCL SAT Solvers
Motivation
Restarts in CDCL SAT solvers are intended to escape the current region of the
search space and begin exploring a new partition. This re-exploration is guided
by the variable decision order, which in learning-rate based heuristics (LRB)
is determined by each variable's reward — its learning rate (LR), reflecting
how often it participates in generating learned clauses.
This raises a critical but overlooked question: if the variable reward ranking
has not changed at the time of a restart, does the restart actually serve its
purpose? If the decision order post-restart is effectively identical to the
one before, the solver will re-enter the same search region, making the restart
semantically meaningless and computationally wasteful.
A further complication arises from how LRB updates rewards. A variable's LR is
updated only when it is unassigned (backtracked). Variables assigned at low
decision levels may survive many hundreds of conflicts without being backtracked,
leaving their LR values frozen and stale. Despite being stale, these values
still directly influence the post-restart variable ordering, since they remain
in the priority queue. Consequently, the stale LRs of non-unassigned variables
are not a minor implementation detail — they are a structural factor that can
cause restarts to reproduce the same decision order and thus the same search
behavior.
This motivates a new condition for meaningful restarts: a restart should only
be triggered (or considered effective) when the LR ranking has shifted
sufficiently to guarantee exploration of a genuinely new region.
Difference from Current Solver Mechanisms
Current restart strategies — including Glucose's LBD-based restarts, reluctant
doubling, and fixed-interval schemes — decide when to restart based on
conflict-level statistics such as clause quality (LBD) or conflict counts. None
of these strategies verify whether the variable reward ordering has actually
changed. They assume that clearing the assignment stack is sufficient to
redirect search, without checking whether the reward landscape that drives
re-exploration is any different from before.
The LRB heuristic itself compounds this gap. Because LR updates are deferred to
unassignment time, variables with long assignment intervals receive a single
coarse batch update at restart, averaging over an extended history. This dilutes
the influence of recent conflict information, potentially reinforcing the old
variable ranking rather than reflecting a fresh perspective on the problem
structure.
The proposed direction departs from current mechanisms in two key ways:
-
Reward-order awareness at restart time: Rather than triggering restarts
purely on conflict statistics, restarts should be conditioned on — or
evaluated against — whether the LR ranking has meaningfully changed.
-
All variables' rewards matter: To assess ranking stability, LR estimates
must be maintained for all variables continuously, including those not yet
unassigned, rather than only updating at backtrack time.
This represents a shift from conflict-count-driven restarts to
reward-landscape-driven restarts, more directly aligned with the semantic
purpose of restarting in CDCL search.
Research Direction: Restart-Aware Reward Consistency in CDCL SAT Solvers
Motivation
Restarts in CDCL SAT solvers are intended to escape the current region of the
search space and begin exploring a new partition. This re-exploration is guided
by the variable decision order, which in learning-rate based heuristics (LRB)
is determined by each variable's reward — its learning rate (LR), reflecting
how often it participates in generating learned clauses.
This raises a critical but overlooked question: if the variable reward ranking
has not changed at the time of a restart, does the restart actually serve its
purpose? If the decision order post-restart is effectively identical to the
one before, the solver will re-enter the same search region, making the restart
semantically meaningless and computationally wasteful.
A further complication arises from how LRB updates rewards. A variable's LR is
updated only when it is unassigned (backtracked). Variables assigned at low
decision levels may survive many hundreds of conflicts without being backtracked,
leaving their LR values frozen and stale. Despite being stale, these values
still directly influence the post-restart variable ordering, since they remain
in the priority queue. Consequently, the stale LRs of non-unassigned variables
are not a minor implementation detail — they are a structural factor that can
cause restarts to reproduce the same decision order and thus the same search
behavior.
This motivates a new condition for meaningful restarts: a restart should only
be triggered (or considered effective) when the LR ranking has shifted
sufficiently to guarantee exploration of a genuinely new region.
Difference from Current Solver Mechanisms
Current restart strategies — including Glucose's LBD-based restarts, reluctant
doubling, and fixed-interval schemes — decide when to restart based on
conflict-level statistics such as clause quality (LBD) or conflict counts. None
of these strategies verify whether the variable reward ordering has actually
changed. They assume that clearing the assignment stack is sufficient to
redirect search, without checking whether the reward landscape that drives
re-exploration is any different from before.
The LRB heuristic itself compounds this gap. Because LR updates are deferred to
unassignment time, variables with long assignment intervals receive a single
coarse batch update at restart, averaging over an extended history. This dilutes
the influence of recent conflict information, potentially reinforcing the old
variable ranking rather than reflecting a fresh perspective on the problem
structure.
The proposed direction departs from current mechanisms in two key ways:
Reward-order awareness at restart time: Rather than triggering restarts
purely on conflict statistics, restarts should be conditioned on — or
evaluated against — whether the LR ranking has meaningfully changed.
All variables' rewards matter: To assess ranking stability, LR estimates
must be maintained for all variables continuously, including those not yet
unassigned, rather than only updating at backtrack time.
This represents a shift from conflict-count-driven restarts to
reward-landscape-driven restarts, more directly aligned with the semantic
purpose of restarting in CDCL search.