This paper introduces SATformer, a novel Transformer-based approach for the Boolean Satisfiability (SAT) problem. Rather than solving the problem directly, SATformer approaches the problem from the opposite direction by focusing on unsatisfiability. Specifically, it models clause interactions to identify any unsatisfiable sub-problems. Using a graph neural network, we convert clauses into clause embeddings and employ a hierarchical Transformer-based model to understand clause correlation. SATformer is trained through a multi-task learning approach, using the single-bit satisfiability result and the minimal unsatisfiable core (MUC) for UNSAT problems as clause supervision. As an end-to-end learning-based satisfiability classifier, the performance of SATformer surpasses that of NeuroSAT significantly. Furthermore, we integrate the clause predictions made by SATformer into modern heuristic-based SAT solvers and validate our approach with a logic equivalence checking task. Experimental results show that our SATformer can decrease the runtime of existing solvers by an average of 21.33%.

翻译：本文提出SATformer——一种基于Transformer的新型布尔可满足性问题求解方法。与直接求解问题不同，SATformer从反向角度聚焦于不可满足性。具体而言，该方法通过建模子句交互来识别任何不可满足子问题。我们利用图神经网络将子句转化为子句嵌入，并采用基于Transformer的层次化模型理解子句关联性。SATformer通过多任务学习方式进行训练，利用单位比特可满足性结果及不可满足问题的最小不可满足核心作为子句监督信号。作为一种端到端基于学习的可满足性分类器，SATformer的性能显著超越NeuroSAT。此外，我们将SATformer生成的子句预测融入现代启发式SAT求解器，并通过逻辑等价性检查任务验证本方法有效性。实验结果表明，SATformer可使现有求解器的运行时间平均降低21.33%。