IB-Net: Initial Branch Network for Variable Decision in Boolean Satisfiability

TL;DR

IB-Net introduces a graph neural network framework that significantly accelerates Boolean SAT solving in Electronic Design Automation, especially for unsatisfiable problems, by achieving notable runtime speedups.

Contribution

The paper presents IB-Net, a novel graph neural network approach with specialized encoding for unsatisfiable SAT problems, improving solver efficiency in EDA workflows.

Findings

Achieves 5.0% average speedup on industrial data

Achieves 8.3% average speedup on SAT competition data

Demonstrates effectiveness across multiple solvers and datasets

Abstract

Boolean Satisfiability problems are vital components in Electronic Design Automation, particularly within the Logic Equivalence Checking process. Currently, SAT solvers are employed for these problems and neural network is tried as assistance to solvers. However, as SAT problems in the LEC context are distinctive due to their predominantly unsatisfiability nature and a substantial proportion of UNSAT-core variables, existing neural network assistance has proven unsuccessful in this specialized domain. To tackle this challenge, we propose IB-Net, an innovative framework utilizing graph neural networks and novel graph encoding techniques to model unsatisfiable problems and interact with state-of-the-art solvers. Extensive evaluations across solvers and datasets demonstrate IB-Net's acceleration, achieving an average runtime speedup of 5.0% on industrial data and 8.3% on SAT competition data empirically. This breakthrough advances efficient solving in LEC workflows.