In this paper, we propose SATformer, a novel Transformer-based solution for
Boolean satisfiability (SAT) solving. Different from existing learning-based
SAT solvers that learn at the problem instance level, SATformer learns the
minimum unsatisfiable cores (MUC) of unsatisfiable problem instances, which
provide rich information for the causality of such problems. Specifically, we
apply a graph neural network (GNN) to obtain the embeddings of the clauses in
the conjunctive normal format (CNF). A hierarchical Transformer architecture is
applied on the clause embeddings to capture the relationships among clauses,
and the self-attention weight is learned to be high when those clauses forming
UNSAT cores are attended together, and set to be low otherwise. By doing so,
SATformer effectively learns the correlations among clauses for SAT prediction.
Experimental results show that SATformer is more powerful than existing
end-to-end learning-based SAT solvers.

本文提出了 SATformer，一种基于 Transformer 的布尔满足性（SAT）求解方法，实现通过学习不可满足问题实例的最小不满足核（MUC），使用图神经网络得到 CNF 中子句的嵌入表示，采用分层 Transformer 体系结构以捕捉这些子句之间的关系，并注重没能同时出现在 UNSAT 核心中的子句的权重，实验结果表明，SATformer 能够优于现有的基于学习的 SAT 求解器。