NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks

TL;DR

NeuroBack tackles the practicality gap in applying Graph Neural Networks to CDCL SAT solving by performing offline phase predictions that focus on backbone variables and are applied before solving on CPU. It introduces DataBack, a large, diverse dataset for backbone-phase labeling, and a Graph Transformer-based GNN to predict backbone phases and transfer knowledge to all variables. Integrated with Kissat as NeuroBack-Kissat, the approach yields measurable improvements on SATCOMP-2022 and SATCOMP-2023, all without GPU involvement during solving. The work demonstrates that offline, backbone-aware phase initialization can meaningfully accelerate large-scale SAT solving and suggests avenues for further dynamic integration and data-driven enhancements.

Abstract

Propositional satisfiability (SAT) is an NP-complete problem that impacts many research fields, such as planning, verification, and security. Mainstream modern SAT solvers are based on the Conflict-Driven Clause Learning (CDCL) algorithm. Recent work aimed to enhance CDCL SAT solvers using Graph Neural Networks (GNNs). However, so far this approach either has not made solving more effective, or required substantial GPU resources for frequent online model inferences. Aiming to make GNN improvements practical, this paper proposes an approach called NeuroBack, which builds on two insights: (1) predicting phases (i.e., values) of variables appearing in the majority (or even all) of the satisfying assignments are essential for CDCL SAT solving, and (2) it is sufficient to query the neural model only once for the predictions before the SAT solving starts. Once trained, the offline model inference allows NeuroBack to execute exclusively on the CPU, removing its reliance on GPU resources. To train NeuroBack, a new dataset called DataBack containing 120,286 data samples is created. NeuroBack is implemented as an enhancement to a state-of-the-art SAT solver called Kissat. As a result, it allowed Kissat to solve up to 5.2% and 7.4% more problems on two recent SAT competition problem sets, SATCOMP-2022 and SATCOMP-2023, respectively. NeuroBack therefore shows how machine learning can be harnessed to improve SAT solving in an effective and practical manner.

Figures (5)

• Figure 1: Overview of NeuroBack. First, the input CNF formula is converted into a compact and more learnable graph representation. A trained GNN model is then applied once on the graph before SAT solving begins for phase selection. The SAT solver utilizes phase information in the resulting labeled graph as an initialization to guide its solving process. Thus, with the offline process of making instructive phase predictions, NeuroBack makes the solving more effective and practical.
• Figure 2: An example graph representation of the CNF formula $(v_1\lor v_2)\land (v_2 \lor v_3 ) \land (v_3 \lor v_4)$. A meta node $m$ is added along with meta edges (represented by dashed lines) connecting to all clause nodes in the connected component, reducing the graph diameter from six to four.
• Figure 3: The architecture of NeuroBack model, consisting of three main components: a GNN subnet with $L$ stacked GNN blocks, a transformer subnet with $M$ GSA transformer blocks and $N$ LSA transformer blocks, and a FFN layer for node classification.
• Figure 4: Progress of Default-Kissat, Random-Kissat, and NeuroBack-Kissat over time in solving problems (time in seconds) on SATCOMP-2022 (left) and SATCOMP-2023 (right), respectively. NeuroBack-Kissat outperforms the two baseline solvers on both testing sets.
• Figure 5: Time taken by Default-Kissat vs. NeuroBack-Kissat on SATCOMP-2022 (a), Random-Kissat vs. NeuroBack-Kissat on SATCOMP-2022 (b), Default-Kissat vs. NeuroBack-Kissat on SATCOMP-2023 (c), and Random-Kissat vs. NeuroBack-Kissat on SATCOMP-2023 (d) to solve each test problem in seconds (for problems that are solved by at least one solver). Each problem is represented by a dot whose location indicates the solving time of each method. The dots on the dashed lines at 5,000 seconds indicate failures. It is evident that more dots are present in the lower triangular areas, indicating that there are more problems on which NeuroBack-Kissat outperforms both Default-Kissat and Random-Kissat.