NeuroComb: Improving SAT Solving with Graph Neural Networks

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 by improving their variable branching heuristics through predictions generated by Graph Neural Networks(GNNs). However, so far this approach either has not made solving more effective, or has required online access to substantial GPU resources. Aiming to make GNN improvements practical, this paper proposes an approach called NeuroComb, which builds on two insights: (1) predictions of important variables and clauses can be combined with dynamic branching into a more effective hybrid branching strategy, and (2) it is sufficient to query the neural model only once for the predictions before the SAT solving starts. NeuroComb is implemented as an enhancement to a classic CDCL solver called MiniSat and a more recent CDCL solver called Glucose. As a result, it allowed MiniSat to solve 11% and Glucose 5% more problems on the recent SATCOMP-2021 competition problem set, with the computational resource requirement of only one GPU. NeuroComb is therefore a both effective and practical approach to improving SAT solving through machine learning.