Reward Defining in Multi-armed Bandit SAT Strategy

SAT solvers are widely used in various fields, and significant efforts have been made to improve the efficiency of Conflict-Driven Clause Learning (CDCL) solvers by integrating the Multi-Armed Bandit (MAB) algorithm. A notable example is the Kissat_MAB solver. However, existing MAB-based solvers face limitations due to their reward functions, which are not wellaligned with the complexities of CDCL SAT solving, leading to biased heuristic selection, especially in challenging instances. To address this, we propose a novel MAB framework, MAB-DC, featuring a new reward function designed to better adapt to SAT solving. This framework is generalizable and can be applied to all MAB-based solvers. Building on the advanced Kissat_MAB solver, we develop Kissat_MAB-DC. Experimental evaluations on 800 instances from SAT 2022 and SAT 2023 demonstrate that Kissat_MAB-DC outperforms Kissat_MAB, Kissat_MABHyWalk, and Kissat_MAB_Conflict+ in terms of both the number of solved instances and average runtime, particularly for satisfiable instances. Additionally, Kissat_MAB-DC achieved second place in the 2024 SAT Competition.