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.

翻译：布尔可满足性问题是电子设计自动化中的关键组成部分，尤其是在逻辑等价性检查流程中。目前，SAT求解器被用于解决这些问题，同时神经网络也被尝试作为辅助工具。然而，由于LEC场景中的SAT问题具有显著的不可满足性特征，且包含大量UNSAT核心变量，现有的神经网络辅助方法在此专业领域未能成功。为应对这一挑战，我们提出IB-Net这一创新框架，利用图神经网络与新型图编码技术对不可满足问题进行建模，并与最先进的求解器进行交互。跨求解器与数据集的广泛评估表明，IB-Net可实现加速效果：在工业数据集上平均运行时间加速5.0%，在SAT竞赛数据集上达到8.3%。这一突破推动了LEC工作流中的高效求解进程。