论文标题
估计SAT编码的硬度，以检查布尔电路的逻辑等效性检查
Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits
论文作者
论文摘要
在本文中，我们调查了如何估计布尔可满足性（SAT）编码的逻辑等效检查问题（LEC）的硬度。在常规的SAT求解器无法在合理的时间内解决SAT实例时，对硬度的有意义的估计很重要。我们表明，可以估计\ textIt {w.r.t。} SAT编码的硬度硬度。我们还证明了结果估计值对与所考虑的分区相关的特殊定义随机变量的概率特征的依赖性。本文提出了几种构造分区的方法，在实践中使用时，它可以很好地估算LEC的SAT编码的硬度。在实验部件中，我们提出了一类可扩展的LEC测试，这些测试具有相对较小的输入尺寸$ n $的考虑到所考虑电路的非常复杂的实例。例如，对于$ n = 40 $，最先进的SAT求解器都无法在合理的时间内应对所考虑的测试。但是，可以使用所提出的分区方法并行解决这些测试。
In this paper we investigate how to estimate the hardness of Boolean satisfiability (SAT) encodings for the Logical Equivalence Checking problem (LEC). Meaningful estimates of hardness are important in cases when a conventional SAT solver cannot solve a SAT instance in a reasonable time. We show that the hardness of SAT encodings for LEC instances can be estimated \textit{w.r.t.} some SAT partitioning. We also demonstrate the dependence of the accuracy of the resulting estimates on the probabilistic characteristics of a specially defined random variable associated with the considered partitioning. The paper proposes several methods for constructing partitionings, which, when used in practice, allow one to estimate the hardness of SAT encodings for LEC with good accuracy. In the experimental part we propose a class of scalable LEC tests that give extremely complex instances with a relatively small input size $n$ of the considered circuits. For example, for $n = 40$, none of the state-of-the-art SAT solvers can cope with the considered tests in a reasonable time. However, these tests can be solved in parallel using the proposed partitioning methods.
