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

arXiv: https://arxiv.org/abs/2405.11024 · HTML: https://mlsanity.com/paper/2405.11024/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 14 of its 49 references that are in the map.
- First posted on arXiv 17 May 2024.

## Builds on (most cited first, 14 of 14)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [Semi-Supervised Classification with Graph Convolutional Networks](https://mlsanity.com/paper/1609.02907/) (2016)
- [Benchmarking Graph Neural Networks](https://mlsanity.com/paper/2003.00982/) (2020)
- [Combinatorial optimization and reasoning with graph neural networks](https://mlsanity.com/paper/2102.09544/) (2021)
- [Deep Graph Library: A Graph-Centric, Highly-Performant Package for Graph Neural Networks](https://mlsanity.com/paper/1909.01315/) (2019)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Automated Algorithm Selection: Survey and Perspectives](https://mlsanity.com/paper/1811.11597/) (2018)
- [Streaming Graph Neural Networks via Continual Learning](https://mlsanity.com/paper/2009.10951/) (2020)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [Machine Learning Methods in Solving the Boolean Satisfiability Problem](https://mlsanity.com/paper/2203.04755/) (2022)
- [G2SAT: Learning to Generate SAT Formulas](https://mlsanity.com/paper/1910.13445/) (2019)
- [HardSATGEN: Understanding the Difficulty of Hard SAT Formula Generation and A Strong Structure-Hardness-Aware Baseline](https://mlsanity.com/paper/2302.02104/) (2023)
- [W2SAT: Learning to generate SAT instances from Weighted Literal Incidence Graphs](https://mlsanity.com/paper/2302.00272/) (2023)

## Built on by (most cited first, 5 of 5)

- [Learning to Solve Weighted Maximum Satisfiability with a Co-Training Architecture](https://mlsanity.com/paper/2511.19544/) (2025)
- [Algorithm Selection with Zero Domain Knowledge via Text Embeddings](https://mlsanity.com/paper/2604.19753/) (2026)
- [Unsat Core Prediction through Polarity-Aware Representation Learning over Clause-Literal Hypergraphs](https://mlsanity.com/paper/2605.04819/) (2026)
- [Learning How to Cube](https://mlsanity.com/paper/2605.16632/) (2026)
- [Synthesizing Feature Extractors: An Agentic Approach for Algorithm Selection](https://mlsanity.com/paper/2608.17170/) (2026)

## Abstract (arXiv)

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.