SATformer: Transformer-Based UNSAT Core Learning

arXiv:2209.00953v2 Announce Type: replace-cross
Abstract: 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 …

abstract arxiv core cs.ai cs.lg cs.lo graph graph neural network identify interactions network neural network novel paper transformer type