Kissat_MAB_CoRephase: Combining Different Rephasing Heuristics Using MAB in SAT

SAT solvers have practical applications across various domains, such as artificial intelligence, software verification, etc. Despite the development of various rephasing strategies, including fixed and Multi-Armed Bandit (MAB) based approaches, a dynamic rephasing strategy that simultaneously increases the number of solved instances and reduces runtime has been lacking. In this paper, we address this gap by proposing a novel rephasing framework based on the MAB technique. Our primary objective is to enhance the efficiency of ConflictDriven Clause Learning (CDCL) solvers, enabling them to handle simple instances more effectively while avoiding local optima in challenging cases. We implemented our method in a solver called Kissat_MAB_CoRephase and evaluated its performance against state-of-the-art solvers, including Kissat-MAB-rephasing, Kissat_MAB, Kissat_MAB-HyWalk, and Kissat_MAB_Conflict+. Experimental results demonstrate that Kissat_MAB_CoRephase significantly outperforms these solvers, achieving a 52% improvement in performance over Kissat_MAB_Conflict+ on solved SAT instances. Specifically, our approach increases the number of solved instances and reduces the average runtime, particularly for satisfiable instances. These findings highlight the effectiveness of our dynamic rephasing strategy in advancing the state-of-theart SAT solvers.