Addressing Variable Dependency in GNN-based SAT Solving
Abstract
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.
Cite
@article{arxiv.2304.08738,
title = {Addressing Variable Dependency in GNN-based SAT Solving},
author = {Zhiyuan Yan and Min Li and Zhengyuan Shi and Wenjie Zhang and Yingcong Chen and Hongce Zhang},
journal= {arXiv preprint arXiv:2304.08738},
year = {2023}
}