Rethinking Clause Management for CDCL SAT Solvers

TL;DR

This paper introduces a new clause reduction method for CDCL SAT solvers that improves performance on complex arithmetic circuit verification by decoupling clause properties, outperforming traditional LBD-based metrics.

Contribution

A novel clause reduction mechanism independent of LBD that separately handles clause lineage and usage, enhancing solver efficiency on complex verification problems.

Findings

Achieves up to 5.74x speedup on complex arithmetic circuit benchmarks

Maintains comparable performance on general-purpose benchmarks

Challenges the effectiveness of LBD as a universal clause quality metric

Abstract

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.