A GRU-Based SAT Phase Prediction Algorithm

Abstract

In the field of computer science, the Boolean Satisfiability Problem (SAT) was the first problem proven to be NP-complete and has been widely applied in artificial intelligence, formal verification, and many other research domains. Most modern SAT solvers are built upon the Conflict-Driven Clause Learning (CDCL) framework, whose performance heavily relies on heuristic mechanisms such as variable branching decisions and phase selection strategies. Although graph neural network-based heuristic guidance has become a popular research direction, existing approaches still suffer from significant limitations when handling large-scale industrial instances, particularly in capturing long-range variable dependencies and achieving sufficient reasoning depth. To address these challenges, this paper proposes NeuroLogic-GSM, a SAT phase prediction model based on Gated Recurrent Units (GRUs). The proposed model reconstructs the traditional static convolution-stacking paradigm into a recurrent iterative reasoning architecture, where weight-shared logical processing units are employed to simulate unit propagation and conflict analysis mechanisms, while GRUs dynamically track the evolution of variable states to effectively capture long-range logical dependencies. The introduction of recurrent reasoning units not only enhances the logical reasoning depth of the model, but also improves parameter utilization efficiency and training stability. Experimental results on the main tracks of the SAT Competitions from 2023 to 2025 demonstrate that NeuroLogic-GSM achieves solver performance improvements of 2.5%, 1.77%, and 1.48%, respectively, compared with NeuroBack, validating its effectiveness in handling complex logical reasoning tasks.