Boolean Satisfiability (SAT) solving underpins a wide range of applications in Electronic Design Automation (EDA), particularly formal verification. However, this paper observes that the mainstream clause reduction heuristic in modern SAT solvers becomes ineffective in the critical domain of complex arithmetic circuit verification, such as multipliers. On these instances, the dominant Literal Block Distance (LBD) metric for measuring clause quality degrades into a simple value of clause length, without any perception of dynamic clause usage during solving.To address this issue, a novel clause reduction mechanism is proposed, which is entirely independent of LBD. Its core idea is to decouple and handle separately the two most fundamental characteristics of learnt clauses--inherent lineage and dynamic usage patterns--thereby avoiding the efficiency degradation caused by inappropriately mixing these properties. Experiments show that our method consistently improves mainstream solvers and achieves speedups of up to 5.74x on complex arithmetic circuit problems, while maintaining comparable performance on general-purpose benchmarks. These results challenge the prevailing LBD-centric clause quality metric for clause management.

翻译：布尔可满足性（SAT）求解是电子设计自动化（EDA）中广泛应用（尤其是形式化验证）的基础技术。然而，本文发现现代SAT求解器中的主流子句约简启发式方法在复杂算术电路（如乘法器）验证这一关键领域中效果不佳。在此类问题上，用于衡量子句质量的主导性指标——文字块距离（LBD）——会退化为简单的子句长度值，完全无法感知求解过程中子句的动态使用情况。为解决这一问题，本文提出了一种全新的子句约简机制，该机制完全独立于LBD。其核心思想是将学习子句的两个最基本特征——固有谱系和动态使用模式——进行解耦与分别处理，从而避免因不恰当地混合这些特性而导致的效率下降。实验表明，我们的方法能持续改进主流求解器，在复杂算术电路问题上实现高达5.74倍的加速，同时在通用基准测试中保持相当的性能。这些结果对当前以LBD为中心的子句质量度量标准提出了挑战。