G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks
This work addresses a crucial gap for researchers in AI and SAT solving by providing a standardized benchmark, though it is incremental as it focuses on evaluation rather than new solver development.
The authors tackled the lack of a unified benchmark for evaluating graph neural network (GNN)-based SAT solvers by introducing G4SATBench, a comprehensive framework with diverse datasets and models, finding that existing GNN models can learn greedy local search strategies but struggle with backtracking search.
Graph neural networks (GNNs) have recently emerged as a promising approach for solving the Boolean Satisfiability Problem (SAT), offering potential alternatives to traditional backtracking or local search SAT solvers. However, despite the growing volume of literature in this field, there remains a notable absence of a unified dataset and a fair benchmark to evaluate and compare existing approaches. To address this crucial gap, we present G4SATBench, the first benchmark study that establishes a comprehensive evaluation framework for GNN-based SAT solvers. In G4SATBench, we meticulously curate a large and diverse set of SAT datasets comprising 7 problems with 3 difficulty levels and benchmark a broad range of GNN models across various prediction tasks, training objectives, and inference algorithms. To explore the learning abilities and comprehend the strengths and limitations of GNN-based SAT solvers, we also compare their solving processes with the heuristics in search-based SAT solvers. Our empirical results provide valuable insights into the performance of GNN-based SAT solvers and further suggest that existing GNN models can effectively learn a solving strategy akin to greedy local search but struggle to learn backtracking search in the latent space. Our codebase is available at https://github.com/zhaoyu-li/G4SATBench.