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.

提出了 IB-Net 框架，利用图神经网络和新颖的图编码技术来模拟不可满足问题，并与先进的求解器交互，以加速解决逻辑等效性检查工作流程，实验证明其平均运行时间提速了 5.0％（工业数据）和 8.3％（SAT 竞赛数据）。

IB-Net: 变量决策的初始分支网络在布尔可满足性中的应用

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

Existing methods provide varying algorithms for different types of Boolean
satisfiability problems (SAT), lacking a general solution framework.
Accordingly, this study proposes a unified framework DCSAT based on integer
programming and reinforcement learning (RL) algorithm to solve different types
of SAT problems such as MaxSAT, Weighted MaxSAT, PMS, WPMS. Specifically, we
first construct a consolidated integer programming representation for four
types of SAT problems by adjusting objective function coefficients. Secondly,
we construct an appropriate reinforcement learning models based on the 0-1
integer programming for SAT problems. Based on the binary tree search
structure, we apply the Monte Carlo tree search (MCTS) method on SAT problems.
Finally, we prove that this method can find all optimal Boolean assignments
based on Wiener-khinchin law of large Numbers. We experimentally verify that
this paradigm can prune the unnecessary search space to find the optimal
Boolean assignments for the problem. Furthermore, the proposed method can
provide diverse labels for supervised learning methods for SAT problems.

该研究提出了一种基于整数规划和强化学习算法的统一框架 DCSAT，用于解决不同类型的布尔可满足性问题，包括 MaxSAT、Weighted MaxSAT、PMS 和 WPMS 等。通过调整目标函数系数，构建了统一的整数规划表示方法，并基于 0-1 整数规划构建了适当的强化学习模型。基于二叉树搜索结构，在 SAT 问题上应用了蒙特卡罗树搜索（MCTS）方法，证明了该方法能够基于维纳 - 欣钦大数定律找到所有最优的布尔赋值。实验证明，该方法能够剪枝不必要的搜索空间，找到问题的最优布尔赋值，同时为 SAT 问题的监督学习方法提供多样的标签。