GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection

TL;DR

GraSS introduces a novel graph neural network approach that leverages domain-specific features and tripartite graph representations to improve SAT solver selection, outperforming existing methods on industrial and benchmark datasets.

Contribution

The paper presents GraSS, a new GNN-based SAT solver selection method that incorporates domain knowledge and runtime-sensitive features for better performance.

Findings

Improved runtime performance over baseline methods.

Effective use of domain-specific graph features.

Successful application to industrial and SAT Competition datasets.

Abstract

Boolean satisfiability (SAT) problems are routinely solved by SAT solvers in real-life applications, yet solving time can vary drastically between solvers for the same instance. This has motivated research into machine learning models that can predict, for a given SAT instance, which solver to select among several options. Existing SAT solver selection methods all rely on some hand-picked instance features, which are costly to compute and ignore the structural information in SAT graphs. In this paper we present GraSS, a novel approach for automatic SAT solver selection based on tripartite graph representations of instances and a heterogeneous graph neural network (GNN) model. While GNNs have been previously adopted in other SAT-related tasks, they do not incorporate any domain-specific knowledge and ignore the runtime variation introduced by different clause orders. We enrich the graph representation with domain-specific decisions, such as novel node feature design, positional encodings for clauses in the graph, a GNN architecture tailored to our tripartite graphs and a runtime-sensitive loss function. Through extensive experiments, we demonstrate that this combination of raw representations and domain-specific choices leads to improvements in runtime for a pool of seven state-of-the-art solvers on both an industrial circuit design benchmark, and on instances from the 20-year Anniversary Track of the 2022 SAT Competition.