# Addressing Variable Dependency in GNN-based SAT Solving

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 7 of its 29 references that are in the map.
- First posted on arXiv 18 Apr 2023.

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

- [Learning Phrase Representations using RNN Encoder-Decoder for Statistical Machine Translation](https://mlsanity.com/paper/1406.1078/) (2014)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Goal-Aware Neural SAT Solver](https://mlsanity.com/paper/2106.07162/) (2021)
- [NLocalSAT: Boosting Local Search with Solution Prediction](https://mlsanity.com/paper/2001.09398/) (2020)
- [DAG-Recurrent Neural Networks For Scene Labeling](https://mlsanity.com/paper/1509.00552/) (2015)
- [Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis](https://mlsanity.com/paper/2107.07116/) (2021)
- [Generalized Equivariance and Preferential Labeling for GNN Node Classification](https://mlsanity.com/paper/2102.11485/) (2021)

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

- [G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks](https://mlsanity.com/paper/2309.16941/) (2023)
- [A Unified Framework for Combinatorial Optimization Based on Graph Neural Networks](https://mlsanity.com/paper/2406.13125/) (2024)
- [Benchmarking Graph Neural Networks in Solving Hard Constraint Satisfaction Problems](https://mlsanity.com/paper/2602.18419/) (2026)

## Abstract (arXiv)

Boolean satisfiability problem (SAT) is fundamental to many applications. Existing works have used graph neural networks (GNNs) for (approximate) SAT solving. Typical GNN-based end-to-end SAT solvers predict SAT solutions concurrently. We show that for a group of symmetric SAT problems, the concurrent prediction is guaranteed to produce a wrong answer because it neglects the dependency among Boolean variables in SAT problems. % We propose AsymSAT, a GNN-based architecture which integrates recurrent neural networks to generate dependent predictions for variable assignments. The experiment results show that dependent variable prediction extends the solving capability of the GNN-based method as it improves the number of solved SAT instances on large test sets.