DualSAT: A Dual-Branch GNN-Transformer Framework for SAT Solving

Existing graph neural network-based methods for Boolean satisfiability (SAT) solving are generally constrained by limited local receptive fields, making it difficult to adequately capture the long-range dependencies between variables and clauses in SAT instances. Moreover, these methods overlook the multi-solution nature of SAT instances. Consequently, their expressive power and generalization performance remain limited. To address these issues, we propose DualSAT, a novel neural framework for the SAT problem, designed to enhance the phase selection heuristic of SAT solvers. Specifically, DualSAT adopts a novel dual-branch graph neural network that separately encodes local structural information and global structural information in the graph, and then fuses them through an attention-based cross-branch feature fusion module. An assignment decision head is further introduced to generate the initial assignment prediction of variables. This prediction process requires only a single forward pass, achieving a favorable balance between expressive power and inference efficiency. Furthermore, to account for the multiple solutions nature of SAT instances, we design a two-stage training strategy that combines supervised and unsupervised learning to improve the generalization performance of the model. Experimental results on multiple datasets show that, as an end-to-end assignment prediction model, DualSAT significantly outperforms NeuroSAT and NeuroBack. In addition, we integrate DualSAT into the classical SAT solver CaDiCaL, where it increases the number of solved instances by up to 11.6% and reduces the number of conflicts by up to 9.21% on SAT competition problem sets.