PaperlayerView exact revision on arXiv

Source-linked AI summary

Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis

Feng Shi, Chonghan Lee, Mohammad Khairul Bashar, Nikhil Shukla, Song-Chun Zhu, Vijaykrishnan Narayanan

arXiv:2107.07116v1cs.NEcs.AIcs.LG

TL;DR

SAT and MaxSAT solving for logic synthesis requires efficient methods for large structured constraint problems. The paper proposes TRSAT, a one-shot Transformer model using meta-path self-attention and bipartite cross-attention, extended with an iterative procedure toward exact SAT solutions. Evaluation reports improved speed over heuristic approaches, improved completion over machine-learning methods, and up to 88.7% completion on DES circuits and 89.3% on arithmetic circuits.

Abstract

from arXiv · show

CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. The increasing popularity of these constraint problems in electronic design automation encourages studies on different SAT problems and their properties for further computational efficiency. There has been both theoretical and practical success of modern Conflict-driven clause learning SAT solvers, which allows solving very large industrial instances in a relatively short amount of time. Recently, machine learning approaches provide a new dimension to solving this challenging problem. Neural symbolic models could serve as generic solvers that can be specialized for specific domains based on data without any changes to the structure of the model. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem, which is the optimization version of SAT where the goal is to satisfy the maximum number of clauses. Our model has a scale-free structure which could process varying size of instances. We use meta-path and self-attention mechanism to capture interactions among homogeneous nodes. We adopt cross-attention mechanisms on the bipartite graph to capture interactions among heterogeneous nodes. We further apply an iterative algorithm to our model to satisfy additional clauses, enabling a solution approaching that of an exact-SAT problem. The attention mechanisms leverage the parallelism for speedup. Our evaluation indicates improved speedup compared to heuristic approaches and improved completion rate compared to machine learning approaches.

I. INTRODUCTION

The paper introduces TRSAT, a Transformer–GNN framework for parallel SAT and MaxSAT solving on heterogeneous bipartite graphs. It combines self-attention, cross-attention, and neural-symbolic methods to improve completion rates and speed in general SAT and CNF-based logic synthesis.

I. INTRODUCTION

  • Traditional heuristic SAT methods can be computationally efficient but remain bounded by greedy, generally sub-optimal search strategies.Prior methods include DPLL-derived conflict-driven clause learning and specialized SAT techniques.Source: §I · p. 1
  • Neural SAT methods avoid some greedy search but often remain sequential, despite clause-level parallelism and correlations through shared variables.This motivates a Transformer-based approach that can exploit parallel processing.Source: §I · p. 1
  • TRSAT combines Transformer and Graph Neural Network architectures to solve CSP/SAT on heterogeneous graphs.The framework is designed to process arbitrary-size instances and approximate CSP/SAT solutions.Source: §I · pp. 1–2
  • Meta-path self-attention models interactions among variables or clauses sharing connections, while cross-attention exchanges information between variables and clauses.These mechanisms operate on the bipartite graph and are intended to improve MaxSAT completion accuracy.Source: §I · pp. 1–2
  • TRSAT combines self- and cross-attention with neural-symbolic methods and reports significant speedup over heuristic SAT solvers and machine-learning methods.The claimed advantage targets CNF-based logic synthesis.Source: §I · p. 2
  • 97% completion for general SAT and 88% for circuit problems are reported, with significant speedup over prior techniques.The reported completion figures summarize the framework’s performance across general and circuit SAT settings.Source: §I · p. 2

II. BACKGROUND

The background establishes CNF encoding for logic gates and relates Transformer attention to graph message passing. It motivates attention-based processing of structured symbolic representations.

A. CNF equations for logic gates

  • Logic gates are converted into CNF by expressing functional equivalence and expanding it into product-of-sums form.The resulting CNF equations are summarized for basic logic gates in Table I [17].Source: A. CNF equations for logic gates · p. 2

B. Transformers and relation to GNNs

  • Transformers use attention instead of recurrence, enabling parallelization while encoding relationships among sequence elements.The paper presents this architecture as a basis for shorter training time.Source: B. Transformers and relation to GNNs · p. 2
  • Transformer self-attention forms a complete query-key connectivity structure, while weak relationships can yield sparse aggregation similar to GNN message passing.Transformer attention is multiplicative through dot products, unlike the additive attention used by GAT [18].Source: B. Transformers and relation to GNNs · p. 2

III. METHODOLOGY

TRSAT represents CNF formulas as polarity-aware bipartite graphs and uses 2-hop meta-paths to connect homogeneous variables or clauses for message passing.

III. METHODOLOGY

  • The methodology combines graph representation, flexible sparse attention, and an overall graph-Transformer architecture for CNF solving.The stated methodology covers CNF graph representation, sparse self- and cross-attention, and the framework architecture.Source: §III · p. 2

A. CNF as bipartite graph and the concept of meta-paths

  • CNF formulas are modeled as undirected bipartite graphs whose nodes are variables and clauses, with edges labeled by positive or negative literal polarity.Separate bi-adjacency matrices A+ and A− store positive and negative incidences.Source: A. CNF as bipartite graph and the… · p. 3
  • 2-hop directed meta-paths let variables or clauses exchange information with same-type nodes that share clauses or variables.The four meta-path types are (+,+), (+,−), (−,+), and (−,−).Source: A. CNF as bipartite graph and the… · p. 3
  • Meta-path adjacency matrices are computed by multiplying positive and negative incidence matrices or their transposes, encoding polarity-specific connectivity.For example, A(+,+) captures positive-positive paths between variables, while A(+,−) captures positive-negative paths.Source: A. CNF as bipartite graph and the… · p. 3

B. Sparse attention and graph Transformer

The model uses sparse, topology-constrained attention on the bipartite graph, within a sequential encoder-decoder Transformer architecture.

B. Sparse attention and graph Transformer

  • Sparse attention computes coefficients only for connected graph-node pairs, then normalizes each score over neighboring nodes with SoftMax.This topology supports efficient sparse matrix multiplication through tensorized feature gathering and scattering.Source: B. Sparse attention and graph… · pp. 3–4
  • TRSAT consists of sequentially connected encoder and decoder layers, with separate encoder and decoder architectures.The architecture is designed for bipartite graph structures.Source: Figure 5 · p. 4
  • Queries, keys, and values are obtained from node features through learned projections Q = XWq, K = YWk, and V = YWv.The formulation supports self-attention when X = Y and cross-attention when X ≠ Y.Source: B. Sparse attention and graph… · pp. 3–4
  • The resulting attention maps are multi-head sparse matrices sharing the topology of a single adjacency matrix, enabling parallel feature aggregation.The implementation uses indexed gathering and scattering operations for sparse matrix multiplication.Source: B. Sparse attention and graph… · p. 4

C. Loss Evaluation

The loss formulation replaces discrete clause satisfaction with differentiable continuous outputs and a smooth approximation, allowing gradient-based training toward satisfiable assignments.

C. Loss Evaluation

  • The model outputs a continuous scalar xi ∈ [0, 1] for each variable because the original CNF satisfaction measure is non-differentiable.Variable assignments are recovered from these continuous outputs using a small stabilizing value ϵ.Source: C. Loss Evaluation · p. 4
  • The method approximates clause disjunctions with max(·) and replaces max with a differentiable smoothmax function.The smoothmax converges to max as τ → ∞, with τ = 5 reported as sufficient in practice.Source: C. Loss Evaluation · p. 4
  • Training maximizes the modified differentiable CNF measure and uses negative log-loss for numerical stability and computational efficiency.The objective is to find a satisfiable assignment for each CSP problem.Source: C. Loss Evaluation · p. 4

D. Heterogeneous Graph Transformer Architecture

TRSAT uses an encoder-decoder Heterogeneous Graph Transformer that combines same-type message aggregation through meta-paths with variable-clause cross-attention.

D. Heterogeneous Graph Transformer Architecture

  • TRSAT uses an adjustable encoder-decoder architecture for heterogeneous graph processing.The architecture is organized into configurable encoder and decoder layers.Source: D. Heterogeneous Graph Transformer… · p. 4
  • Encoder layers apply self-attention over same-type nodes connected through meta-paths, followed by residual connections and layer normalization.Variables and clauses exchange same-type information indirectly because the bipartite graph lacks direct homogeneous edges.Source: D. Heterogeneous Graph Transformer… · pp. 4–5
  • Decoder layers use cross-attention to pass weighted messages between variables and clauses before residual normalization and feed-forward enhancement.The heterogeneous attention distinguishes variable and clause node types.Source: D. Heterogeneous Graph Transformer… · p. 5

E. Analysis of the Complexity

The model’s sparse attention has complexity linear in graph nodes and edges, while an iterative procedure removes solved clauses and related variables to extend MaxSAT assignments toward exact SAT.

E. Analysis of the Complexity

  • O(|E| × |F|) attention computation and linear node-edge memory make sparse self- and cross-attention scale with graph size.The node encoding and feed-forward modules add O(|V| × F × F′) time, and total attention-head complexity is proportional to nodes and edges.Source: E. Analysis of the Complexity · p. 5

F. MaxSAT approximates Exact SAT

  • MaxSAT approximates exact SAT by repeatedly applying one-shot TRSAT, identifying unsolved clauses, and removing solved clauses with related variables.The iterative algorithm outputs assignments for variables accumulated across successive reduced problems.Source: F. MaxSAT approximates Exact SAT · p. 5
  • Unlike PDP’s decimation, the procedure reduces problem scale by conditionally removing solved clauses and their related variables.The paper associates this scale reduction with faster and more efficient solution generation.Source: F. MaxSAT approximates Exact SAT · p. 5

IV. EXPERIMENTS EVALUATION

The experiments cover four synthetic CSP/SAT problem classes and CNF translations of real hardware circuits, comparing TRSAT with stochastic, reinforcement-learning, and graph-neural baselines.

A. Dataset

  • The training set spans random 3-SAT, graph coloring, vertex cover, and clique detection distributions.It includes 1,200 SATLIB formulas and 4,000 generated instances for each of the three graph-specific problems.Source: A. Dataset · p. 5
  • The logic-synthesis evaluation uses DES and arithmetic circuit datasets translated into CNF, with largest instances averaging 14K variables and 42K clauses.The arithmetic circuits include adder trees and Braun multipliers.Source: A. Dataset · p. 5

B. Baselines

  • TRSAT is evaluated against WalkSAT and Glucose, RLSAT, and PDP across CSP/SAT solving and CNF-based logic synthesis.These baselines represent stochastic local search, reinforcement-learning SAT solving, and hybrid recurrent/graph neural approaches.Source: B. Baselines · pp. 5–6

C. Experimental Configuration

Experiments use GPU-parallel implementations and compare TRSAT with RLSAT and PDP on completion rate, learning behavior, and inference speed across general CSP/SAT tasks.

C. Experimental Configuration

  • Experiments run on a Ryzen 7 3700X CPU with an RTX 2080 GPU, deploying parallelizable models on the GPU while sequential baselines remain CPU-bound.The implementation uses PyTorch and PyTorch Geometric for graph representation learning and GPU computation.Source: C. Experimental Configuration · p. 6

1) General CSP/SAT solving:

  • TRSAT achieves higher completion rate than RLSAT after training for 500 epochs on the selected datasets.Its arbitrary-size processing also permits combining multiple distributions of one problem class into a single training dataset.Source: 1) General CSP/SAT solving · p. 6, Table III · p. 7
  • TRSAT maintains more stable validation behavior than RLSAT as graph scales change during training.RLSAT’s reinforcement-learning exploration on new graph scales produces oscillating validation performance, whereas TRSAT updates all graph nodes in parallel.Source: 1) General CSP/SAT solving · p. 6, Figure 6 · p. 6
  • TRSAT achieves higher average test speeds than PDP regardless of graph structure while retaining a high clause-assignment completion rate.The paper attributes this efficiency to homogeneous-node communication, which supplies semantic information and reduces message-passing iterations.Source: Figure 7 · p. 6, 1) General CSP/SAT solving · p. 7, Table IV · p. 7

2) CNF-based logic synthesis:

TRSAT delivers high completion rates for CNF-based circuit instances and targets acceleration through low-latency, parallel inference. Paired with a deterministic solver, it provides speedup across diverse circuit structures and instance sizes.

  • TRSAT achieves average completion rates of 88.7% for DES circuits and 89.3% for arithmetic circuits after 500 training epochs.The evaluation uses WalkSAT and Glucose as authoritative baselines.Source: 2) CNF-based logic synthesis · p. 7
  • The model’s latency is evaluated for acceleration rather than completion-rate comparison, because heuristic solvers eventually solve all problems without time limits.Source: 2) CNF-based logic synthesis · p. 7
  • TRSAT paired with a slower deterministic solver provides substantial overall speedup while ensuring a solution.Figure 8 compares average solve speeds against Glucose, using WalkSAT performance as the metric.Source: 2) CNF-based logic synthesis · p. 7, Figure 8 · p. 7
  • The speedup holds regardless of circuit structure, while varied variable and clause distributions demonstrate scalability across logic-synthesis tasks of different difficulties.The main architecture is unchanged across these instances.Source: 2) CNF-based logic synthesis · p. 8

V. CONCLUSION

The paper introduces TRSAT, a one-shot Transformer-based solver for MaxSAT and logic synthesis on bipartite graphs. It combines homogeneous meta-path attention with heterogeneous cross-attention, achieving parallelism, completion rate, and generality across arbitrary-size instances.

  • TRSAT is a one-shot Transformer-derived model for solving MaxSAT on bipartite graph structures.Source: §V · p. 8
  • The framework uses meta-path self-attention among same-type nodes and bipartite cross-attention between literals and clauses.Source: §V · p. 8
  • Experiments report competitive performance and generality, with exceptional parallelism and completion rate on arbitrary-size MaxSAT graphs.Source: §V · p. 8
Loading 2107.07116v1…