布尔电路逻辑等价性检验中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的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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
