A Reinforcement Learning based Reset Policy for CDCL SAT Solvers
Chunxiao Li, Charlie Liu, Jonathan Chung, Zhengyang Lu, Piyush Jha, Vijay Ganesh
TL;DR
This work tackles the challenge of optimally timing resets in CDCL SAT solvers by casting the decision as a non-stationary multi-armed bandit problem. It develops RL-based policies, notably Thompson Sampling (with decay) and UCB variants, to switch between traditional restarts and resets, and introduces partial resets that preserve the top-$k$ variable activities. Across multiple state-of-the-art solvers and benchmark suites (Satcoin and SAT Competition Main Track), the Thompson-based reset policies, especially with decaying shape parameters, yield strong improvements, including solving all Satcoin instances in some configurations and outperforming baselines in several tracks. Theoretical insights reveal exponential separation between full and partial reset regimes and justify the decay mechanism to maintain exploration, underscoring the practical significance of adaptive reset control for SAT solving.
Abstract
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. $Ω(n)$-length partial resets.