基于半张量积的AllSAT求解器设计
A Semi-Tensor Product Based All Solutions Boolean Satisfiability Solver
-
摘要:研究背景 布尔可满足性问题(SAT)求解器在电子设计自动化(EDA)中作为约束求解引擎被广泛使用。目前大多数SAT求解器基于冲突驱动子句学习(CDCL)策略，适用于高效解决工业级大规模问题，而基于数理计算的SAT求解器并没有得到有效的设计和应用。随着计算机科学和数学的发展，结合矩阵和逻辑值的半张量积概念引起研究者们的广泛关注。半张量积与SAT中数理逻辑推理和计算理论方面高度契合，具有重要研究价值。目的 我们的研究目标是，设计一种基于半张量积的数理计算SAT求解器。约束问题的求解可以将SAT问题分为两种情况，SAT及其变种，即全解SAT (AllSAT)。SAT是基于启发式算法的求解，能在最快的时间内得到一个满足约束的解；相比AllSAT基于精确算法，可以得到所有满足约束的解，但很难在大规模实例中得到应用。在EDA逻辑综合中组合电路优化时，不需要功能强大的单实例SAT求解器，开发一个更灵活、鲁棒性好、轻量级的SAT求解器可以更好地处理逻辑综合中产生的一系列小规模电路问题。方法 我们提出了一个实现多个逻辑矩阵的半张量积相乘的SAT求解框架，通过C++语言实现了所提出的算法并集成到了开源综合工具ALSO中，运行“sat”命令即可对任意给定输入约束进行AllSAT求解并且报告所有可满足的解及对应数量。结果 我们的方法对于小规模的电路的SAT求解具有极大的优势，通过对MCNC中的18个基准电路开展实验，结果表明，对于CNF输入而言，同目前最好的方法相比，我们的方法可以平均加速8.1倍；对于电路信息格式输入而言，我们的方法可以平均加速19.9倍。结论 相比于传统的基于启发式算法的SAT求解器，我们提出了一种全新的基于矩阵半张量积的AllSAT求解器。其将逻辑矩阵视为逻辑网络中的原语，同时兼容电路信息和CNF作为输入，具有更广泛的应用场景。与最先进的SAT求解器（MiniSAT和BCAllSAT）的比较表明，我们的求解器具有更好的鲁棒性，并且可以更快地获得所有精确解。Abstract: Boolean satisfiability (SAT) is widely used as a solver engine in electronic design automation (EDA). Typically, SAT is used to determine whether one or more groups of variables can be combined to form a true formula. All solutions SAT (AllSAT) is a variant of the SAT problem. In the fields of formal verification and pattern generation, AllSAT is particularly useful because it efficiently enumerates all possible solutions. In this paper, a semi-tensor product (STP) based AllSAT solver is proposed. The solver can solve instances described in both the conjunctive normal form (CNF) and circuit form. The implementation of our method differs from incremental enumeration because we do not add blocking conditions for existing solutions, but rather compute the matrices to obtain all the solutions in one pass. Additionally, the logical matrices support a variety of logic operations. Results from experiments with MCNC benchmarks using CNF-based and circuit-based forms show that our method can accelerate CPU time by 8.1x (238x maximum) and 19.9x (72x maximum), respectively.
下载: