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.

翻译：布尔可满足性问题（SAT）是众多应用的基础。现有研究已采用图神经网络（GNN）进行（近似）SAT求解。典型的基于GNN的端到端SAT求解器会并发预测SAT解。我们证明，对于一组对称的SAT问题，并发预测必然产生错误答案，因其忽略了SAT问题中布尔变量之间的依赖性。为此，我们提出AsymSAT——一种集成循环神经网络以生成变量赋值依赖预测的GNN架构。实验结果表明，依赖变量预测能增强GNN方法的求解能力，在大型测试集上显著提升可求解SAT实例的数量。