IB-Net: Initial Branch Network for Variable Decision in Boolean Satisfiability
This work addresses a specialized problem in Electronic Design Automation for engineers and researchers, representing an incremental improvement with domain-specific impact.
The paper tackles the challenge of applying neural network assistance to Boolean Satisfiability problems in Logic Equivalence Checking, where existing methods fail due to the distinctive nature of these problems (predominantly unsatisfiable with many UNSAT-core variables). The proposed IB-Net framework achieves average runtime speedups of 5.0% on industrial data and 8.3% on SAT competition data.
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.