MHQ-SAT: An End-to-End SAT Solver with a Multi-Head Hierarchical Query Mechanism

Abstract

The Boolean Satisfiability Problem (SAT), as a representative NP-complete problem, plays a crucial role in integrated circuit verification, automated reasoning, and combinatorial optimization. In recent years, end-to-end SAT solvers based on graph neural networks (GNNs) have alleviated the reliance on handcrafted heuristics by learning the structural relationships between variables and clauses. However, existing neural SAT solvers with query-based mechanisms typically rely on a single query perspective, which limits their ability to capture diverse reasoning paths within complex constraint structures. As a result, their reasoning stability and generalization performance on large-scale instances remain insufficient. To address these limitations, this paper proposes MHQ-SAT, an end-to-end SAT solving model based on a multi-head hierarchical query mechanism. Built upon the QuerySAT framework, MHQ-SAT introduces a multi-head variable query mechanism and clause-level hierarchical attention modeling. By constructing multiple query perspectives in parallel, the proposed model enhances the expressive capacity of implicit reasoning processes. Meanwhile, a clause-level attention mechanism is employed to dynamically characterize the relative importance of different clauses during reasoning, enabling the model to focus on critical constraint structures. Furthermore, MHQ-SAT integrates query-driven clause updates with gated variable update mechanisms, achieving efficient information interaction between variables and clauses as well as stable iterative reasoning. Extensive experiments on randomly generated 3-SAT and k-SAT benchmarks demonstrate that MHQ-SAT consistently outperforms NeuroSAT, QuerySAT, and other baseline methods across various variable scales and reasoning step settings. In particular, on medium- and large-scale SAT instances, MHQ-SAT exhibits superior robustness and reasoning stability in terms of solution accuracy and the proportion of unsolved instances. Ablation studies further validate the effectiveness of the multi-head query mechanism and clause-level hierarchical modeling in improving overall performance. These results indicate that the proposed multi-head hierarchical query mechanism provides an effective and learnable reasoning enhancement paradigm for end-to-end SAT solving.