Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

SATformer: Transformer-Based UNSAT Core Learning

Zhengyuan Shi, Min Li, Yi Liu, Sadaf Khan, Junhua Huang, Hui-Ling Zhen, Mingxuan Yuan, Qiang Xu

TL;DR

SATformer models clause interactions to identify any unsatisfiable sub-problems and integrates the clause predictions made by SATformer into modern heuristic-based SAT solvers and validate the approach with a logic equivalence checking task.

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 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-Based UNSAT Core Learning

TL;DR

SATformer models clause interactions to identify any unsatisfiable sub-problems and integrates the clause predictions made by SATformer into modern heuristic-based SAT solvers and validate the approach with a logic equivalence checking task.

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 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%.
Paper Structure (21 sections, 14 equations, 5 figures, 8 tables, 1 algorithm)

This paper contains 21 sections, 14 equations, 5 figures, 8 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related Work
  3. Deep Learning for SAT Solving
  4. Transformer and Self-attention Mechanism
  5. SATformer
  6. Boolean Satisfiability Problem
  7. Overview
  8. Training Objective
  9. Hierarchical Design
  10. Combination with SAT solvers
  11. Background on SAT Solvers
  12. Hybrid Solver Design
  13. Experiments
  14. Experimental setting
  15. Performance Comparison with NeuroSAT
  16. ...and 6 more sections

Figures (5)

  • Figure 1: An example of Literal-Clause Graph (LCG).
  • Figure 2: An overview of the model architecture.
  • Figure 3: The architecture of the hierarchical Transformer-based model.
  • Figure 4: Two special unsatisfiable cases in hierarchical structure
  • Figure 5: The runtime reduction of SATformer on CaDiCal queue2019cadical (upper) and Kissat fleury2020cadical (below)