A Reinforcement Learning based Reset Policy for CDCL SAT Solvers
Chunxiao Li Charlie Liu Jonathan Chung Zhengyang Lu Piyush Jha Vijay Ganesh
Restart policy is an important technique used in modern Conflict-Driven
Clause Learning (CDCL) solvers, wherein some parts of the solver state are
erased at certain intervals during the run of the solver. In most solvers,
variable activities are preserved across restart boundaries, resulting in
solvers continuing to search parts of the assignment tree that are not far from
the one immediately prior to a restart. To enable the solver to search possibly
"distant" parts of the assignment tree, we study the effect of resets, a
variant of restarts which not only erases the assignment trail, but also
randomizes the activity scores of the variables of the input formula after
reset, thus potentially enabling a better global exploration of the search
space.
  In this paper, we model the problem of whether to trigger reset as a
multi-armed bandit (MAB) problem, and propose two reinforcement learning (RL)
based adaptive reset policies using the Upper Confidence Bound (UCB) and
Thompson sampling algorithms. These two algorithms balance the
exploration-exploitation tradeoff by adaptively choosing arms (reset vs. no
reset) based on their estimated rewards during the solver's run. We implement
our reset policies in four baseline SOTA CDCL solvers and compare the baselines
against the reset versions on Satcoin benchmarks and SAT Competition instances.
Our results show that RL-based reset versions outperform the corresponding
baseline solvers on both Satcoin and the SAT competition instances, suggesting
that our RL policy helps to dynamically and profitably adapt the reset
frequency for any given input instance. We also introduce the concept of a
partial reset, where at least a constant number of variable activities are
retained across reset boundaries. Building on previous results, we show that
there is an exponential separation between O(1) vs. $\Omega(n)$-length partial
resets.