GMTSAT: A Neural SAT Solver Based on Multi-Slot Global Updates and Gated Message Passing

Abstract

The Boolean Satisfiability Problem (SAT) is a fundamental NP-complete problem in computer science, with broad applications in formal verification, electronic design automation, and combinatorial optimization. In recent years, neural SAT solvers based on message-passing neural networks (MPNNs) have shown promise in variable assignment prediction and heuristic guidance. However, their reliance on local graph topology severely limits their ability to capture long-range logical dependencies. To address this limitation, this paper proposes GMTSAT, a novel neural SAT solving architecture that integrates multi-slot global attention with gated message passing to enhance global reasoning capability and representation robustness. Specifically, we introduce a set of learnable global latent slots that are independent of the underlying graph topology. Through Transformer-based cross-attention and self-attention mechanisms, these slots enable single-step global information aggregation and broadcast across the entire graph while preserving permutation invariance. In addition, a gated residual perceptron is designed to replace conventional MLPs in the message-passing process, effectively suppressing noisy signals and improving training stability. Extensive experiments on large-scale random 3-SAT benchmarks demonstrate that GMTSAT significantly outperforms strong baselines such as NeuroSAT and TG-SAT in variable assignment prediction accuracy, while exhibiting superior scalability to larger problem instances. Ablation studies confirm the independent effectiveness and complementary benefits of the proposed global slot mechanism and gating modules. Furthermore, joint experiments with the state-of-the-art CDCL solver Kissat systematically evaluate two application paradigms: a hard-constraint strategy that aggressively fixes high-confidence variables to reduce the search space, and a soft-constraint guidance strategy that preserves solver completeness while achieving consistent speedups. The results indicate that GMTSAT provides an effective and scalable paradigm for deep integration between neural reasoning models and traditional SAT solvers.