Comprehensive Analysis of Restart Strategies of CDCL SAT Solver

SAT solver based on CDCL has been widely used in formal verification. As the numerous restart strategies and complex parameters, choosing the default strategy reduces the efficiency and usability. In order to improve the practicability of CDCL algorithms, this paper analyzes how restart strategies effect solving performance, and relationship between the initial feature sets and the restart strategy sets. Results demonstrate that the gap between the optimal solution and default solving performance reaches 6959%, on average, 441%; Great individual differences and certain group differences on choosing restart strategies are shown; Compared to restart frequency, restart schedule plays a greater role in solving performance; Changing the restart strategy can improve the solving performance. In addition, seven restart strategies can cover 97% of the optimal strategies. The correlation between the change frequency of the features and the seven strategies provides technical support for choosing the optimal restart strategy.