PaperlayerView exact revision on arXiv

Source-linked AI summary

SATformer: Transformer-Based UNSAT Core Learning

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

arXiv:2209.00953v2cs.AIcs.LGcs.LO

TL;DR

SATformer addresses SAT-solving difficulties in selecting heuristics for satisfiable versus unsatisfiable instances by learning clause interactions and UNSAT cores. It combines GNN clause embeddings, hierarchical Transformer modeling, and multi-task supervision, then uses clause predictions to guide solver initialization. It outperforms NeuroSAT and accelerates UNSAT solving, while its current limitation is that it does not improve satisfiable-instance solving.

Abstract

from arXiv · show

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%.

I. INTRODUCTION

SATformer addresses the difficulty of selecting effective SAT heuristics by predicting satisfiability through clause interactions and UNSAT-core identification. It combines hierarchical Transformer modeling, multi-task supervision, and solver integration to accelerate UNSAT solving.

I. INTRODUCTION

  • SATformer targets manual satisfiability-mode selection and the lack of dedicated UNSAT heuristics, which can increase solving time by up to 50%.These issues matter especially in EDA applications where many instances are UNSAT.Source: §I · p. 1
  • SATformer reframes UNSAT detection as identifying an unsatisfiable sub-problem through interactions among clauses.An UNSAT Core is a subset of clauses whose sub-problem is itself unsatisfiable.Source: §I · p. 1
  • The model uses GNN clause embeddings, a hierarchical Transformer for clause correlations, and dual supervision from satisfiability labels and minimal unsatisfiable cores.The hierarchical design captures relationships among incrementally formed clause groups rather than only pairwise dependencies.Source: §I · pp. 1–2
  • SATformer converts clause prediction scores into variable priorities used to initialize modern SAT solvers through existing branching-priority interfaces.The approach was evaluated by augmenting CaDiCaL and Kissat.Source: §I · p. 1
  • The paper’s contributions include clause-correlation modeling, minimal-UNSAT-core supervision, and a learning-enhanced initialization heuristic for SAT solvers.The introduction presents these as complementary components of the SATformer framework.Source: §I · pp. 1–2

II. RELATED WORK

Prior work spans standalone learning-based SAT solvers, learning-aided heuristics, and Transformer-based graph modeling. The paper then defines SAT through CNF and Literal-Clause Graph representations, motivating UNSAT-core learning as its central approach.

A. Deep Learning for SAT Solving

  • Standalone learning-based SAT solvers predict satisfiability or assignments, but their performance lags modern non-learning solvers because probabilistic predictions do not directly match deterministic SAT reasoning.Examples include NeuroSAT [22], DG-DAGRNN, and DeepSAT [24].Source: A. Deep Learning for SAT Solving · p. 2
  • Learning-aided solvers replace or augment manually designed heuristics, with examples achieving runtime or iteration reductions while remaining generally non-specific to a particular problem type.NLocalSAT [25], Graph-Q-SAT, NeuroCore, and NeuroComb illustrate this direction.Source: A. Deep Learning for SAT Solving · p. 2

B. Transformer and Self-attention Mechanism

  • Transformers model correlations among input tokens through self-attention, and SATformer applies this idea to clauses treated as a non-ordered sequence.Earlier work applied Transformers to MaxSAT using bipartite graph representations [33].Source: B. Transformer and Self-attention… · p. 2

A. Boolean Satisfiability Problem

  • SAT formulas use variables and negated variables as literals, disjunctions of literals as clauses, and conjunctions of clauses as CNF instances.CNF conversion can preserve equivalence in linear time.Source: A. Boolean Satisfiability Problem · p. 2
  • The Literal-Clause Graph represents a CNF formula with literal and clause nodes connected by literal-clause and literal-negation edges.Fig. 1 illustrates this bipartite representation.Source: A. Boolean Satisfiability Problem · p. 2, Figure 1 · p. 2
  • An UNSAT core is a subset of clauses forming an unsatisfiable sub-problem, and extracting such cores can determine whether the original CNF instance is unsatisfiable.The paper therefore learns clause contributions to UNSAT before modeling their interactions.Source: A. Boolean Satisfiability Problem · pp. 2–3

B. Overview

SATformer first derives clause and literal representations, then predicts clause contributions to the UNSAT core and models clause relationships with a hierarchical Transformer.

B. Overview

  • A GNN produces clause and literal embeddings from the CNF instance through message passing on the literal-clause graph.Clause embeddings incorporate information from their involved literals, while literal embeddings incorporate information from connecting clauses.Source: B. Overview · p. 3
  • An MLP predicts each clause’s probability of belonging to the UNSAT core, highlighting clauses that contribute more to unsatisfiability.The classifier is intended to prioritize informative clauses rather than classify every clause perfectly.Source: B. Overview · p. 3
  • The hierarchical Transformer groups clauses incrementally to capture multi-clause interactions that standard Transformers’ pairwise correlations may miss.This design targets unsatisfiability arising from relationships among multiple clauses rather than isolated clause pairs.Source: B. Overview · p. 3

C. Training Objective

SATformer jointly learns clause-level UNSAT-core contributions and instance-level satisfiability, using related supervision signals to improve prediction.

C. Training Objective

  • Multi-task learning trains SATformer simultaneously on UNSAT-core clause prediction and binary satisfiability prediction.Task-clause identifies clauses contributing to unsatisfiability, while Task-sat predicts the final satisfiability result.Source: C. Training Objective · p. 3
  • Minimal unsatisfiable cores provide clause-level targets indicating which clauses belong to an MUC.Although UNSAT cores are not unique, the paper uses minimal cores because only a few smallest combinations are typically possible.Source: C. Training Objective · p. 3
  • For satisfiable instances, the clause target vector contains all zeroes, whereas unsatisfiable instances assign ones to clauses included in the MUC.The clause predictions form a probability distribution whose larger values indicate greater likelihood of forming the MUC.Source: C. Training Objective · p. 3
  • The satisfiability task uses single-bit supervision with Binary Cross-Entropy loss, while the clause task is trained with Kullback-Leibler divergence.The overall objective is a weighted sum of the clause and satisfiability losses.Source: C. Training Objective · p. 3

D. Hierarchical Design

The hierarchical design addresses multi-clause unsatisfiability by repeatedly grouping clause embeddings and applying Transformer attention across progressively coarser levels.

D. Hierarchical Design

  • The hierarchical Transformer captures correlations among clauses by applying self-attention and consolidating clause representations into group embeddings.Its hierarchy is intended to model causes of unsatisfiability involving multiple clauses rather than only clause pairs.Source: D. Hierarchical Design · pp. 3, 5
  • At least three clauses may be required to establish unsatisfiability, making direct multi-token dependency modeling impractical in one Transformer block.The model therefore uses Attention Units that merge clauses within fixed-size windows and relate the resulting groups at higher levels.Source: D. Hierarchical Design · pp. 3–4
  • For n = 11 clauses and window size w = 4, random padding creates D1 = 3 first-level windows.Padding extends the embedding matrix to a length divisible by the window size before grouping.Source: D. Hierarchical Design · p. 4
  • Each hierarchy level forms clause groups from lower-level embeddings, with higher levels learning relationships among those groups.The final representation combines level embeddings and the final clause-group embedding for satisfiability prediction.Source: D. Hierarchical Design · pp. 4–5
  • A window of size w groups clauses into local embeddings, allowing higher-level groups to combine information from broader clause sets.The example groups C1–C3, C4–C6, and subsequent clauses before modeling relationships between groups.Source: D. Hierarchical Design · p. 4

IV. COMBINATION WITH SAT SOLVERS

SATformer is used as an initialization heuristic alongside non-learning SAT solvers, including CaDiCal and Kissat.

IV. COMBINATION WITH SAT SOLVERS

  • The paper combines SATformer with two modern SAT solvers, CaDiCal and Kissat, as an initialization heuristic.This section places the learning-based model within a hybrid solver pipeline alongside non-learning heuristics.Source: §IV · p. 5

A. Background on SAT Solvers

Modern SAT solvers use conflict-driven search and variable heuristics to reduce the search space, but their heuristic scores are generated only during solving.

  • Conflict-Driven Clause Learning adds clauses derived from conflicts, introducing constraints that can substantially reduce the search space, especially for UNSAT problems.Source: A. Background on SAT Solvers · p. 5
  • VSIDS prioritizes variables involved in many conflicts, but its scores are computed online and lack an efficient initialization strategy.Source: A. Background on SAT Solvers · p. 5

B. Hybrid Solver Design

SATformer supplies satisfiability and clause-level UNSAT predictions to initialize modern solvers’ variable heuristics. The experiments evaluate classification, model settings, and solver integration under controlled datasets and configurations.

B. Hybrid Solver Design

  • SATformer predicts satisfiability and clause contributions to unsatisfiability, treating high-contribution clauses as likely sources of conflicts.Source: B. Hybrid Solver Design · p. 5
  • Clause predictions are converted into variable conflict scores using the variable–clause adjacency matrix.Source: B. Hybrid Solver Design · p. 5
  • The resulting variable scores initialize VSIDS through existing solver interfaces, allowing SATformer to operate as a plug-in without modifying the solvers.Source: B. Hybrid Solver Design · p. 5

V. EXPERIMENTS

  • The experimental program compares standalone classification with NeuroSAT, ablates model components, and integrates SATformer with CaDiCaL and Kissat for hard LEC instances.Source: §V · p. 5

A. Experimental setting

  • The evaluation includes binary classification accuracy on balanced satisfiable and unsatisfiable datasets spanning SR(3-10), SR(20), SR(40), and SR(60).Training uses 10K satisfiable and 10K unsatisfiable instances, while default test sets contain 50 instances of each class per scale.Source: A. Experimental setting · p. 5
  • SATformer uses a GNN with 10 message-passing iterations and a four-level hierarchical Transformer, while requiring fewer FLOPs than NeuroSAT despite having more trainable parameters.Source: A. Experimental setting · pp. 5–6

B. Performance Comparison with NeuroSAT

SATformer outperforms NeuroSAT across the tested classification datasets and benefits from clause-focused Transformer attention. Its clause-correlation modeling also supports better performance as instance difficulty decreases.

B. Performance Comparison with NeuroSAT

C. Effectiveness of Transformer Blocks

D. Effectiveness of Hierarchical Transformer

Hierarchical aggregation enables SATformer to capture multi-clause unsatisfiable patterns that plain Transformer stacking may miss. UNSAT-core supervision further benefits the model because clause contributions retain information relevant to SAT solving.

D. Effectiveness of Hierarchical Transformer

E. Effectiveness of Multi-task Learning Strategy

F. Combination with SAT Solvers

SATformer is integrated with CaDiCaL and Kissat as an initialization heuristic, improving UNSAT-solving efficiency while adding little inference overhead. Its benefits are substantial on average but can reverse when a smaller UNSAT core requires harder search.

F. Combination with SAT Solvers

  • 21.64% and 7.60% speedups are achieved by CaDiCaL and Kissat with SATformer on UNSAT instances, respectively.The evaluation uses 60 industrial LEC instances, evenly split between SAT and UNSAT cases, and includes model inference time.Source: F. Combination with SAT Solvers · p. 7, Table VII · p. 8
  • SATformer adds only 0.51% and 0.53% inference overhead to CaDiCaL and Kissat, respectively, while SAT instances show limited benefit and occasional degradation.For CaDiCaL, SATformer takes 30.77% more runtime on SAT instances, but average times are nearly identical: 6.62s with versus 6.63s without SATformer.Source: F. Combination with SAT Solvers · pp. 7–8

G. Failure Case Analysis and Discussion

  • For some instances, SATformer finds smaller UNSAT cores yet increases backtracking, producing small but harder-to-prove cores and reducing runtime efficiency.On C1 and C2, lemma reductions of 7.29% and 29.12% correspond to runtime reductions of 10.06% and 18.07%; C3 and C4 instead require more search.Source: G. Failure Case Analysis and Discussion · p. 8, Table VIII · p. 8

VI. CONCLUSION

  • SATformer’s conclusion reports average solving-time reductions of 21.33% for CaDiCaL and 7.60% for Kissat on logic equivalence checking.The framework is presented as an end-to-end satisfiability classifier and an initialization heuristic for modern SAT solvers.Source: §VI · p. 8

Related papers

Loading 2209.00953v2…