Addressing Variable Dependency in GNN-based SAT Solving
This addresses a specific bottleneck in SAT solving for applications relying on Boolean satisfiability, though it is incremental as it builds on existing GNN methods.
The paper tackled the problem of variable dependency in GNN-based SAT solving, showing that concurrent prediction fails for symmetric SAT problems, and proposed AsymSAT with recurrent neural networks to improve solving capability, increasing the number of solved SAT instances on large test sets.
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.