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

arXiv: https://arxiv.org/abs/2403.03517 · HTML: https://mlsanity.com/paper/2403.03517/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 6 of its 22 references that are in the map.
- First posted on arXiv 6 Mar 2024.

## Builds on (most cited first, 6 of 6)

- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Combinatorial Optimization with Graph Convolutional Networks and Guided Tree Search](https://mlsanity.com/paper/1810.10659/) (2018)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [Learning to Select Cuts for Efficient Mixed-Integer Programming](https://mlsanity.com/paper/2105.13645/) (2021)
- [NLocalSAT: Boosting Local Search with Solution Prediction](https://mlsanity.com/paper/2001.09398/) (2020)
- [WGCN: Graph Convolutional Networks with Weighted Structural Features](https://mlsanity.com/paper/2104.14060/) (2021)

## Abstract (arXiv)

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.