Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Rethinking Clause Management for CDCL SAT Solvers

Yalun Cai, Xindi Zhang, Zhengyuan Shi, Mengxia Tao, Qiang Xu

TL;DR

A novel clause reduction mechanism is proposed, which is entirely independent of Literal Block Distance, 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.

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.

Rethinking Clause Management for CDCL SAT Solvers

TL;DR

A novel clause reduction mechanism is proposed, which is entirely independent of Literal Block Distance, 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.

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.
Paper Structure (23 sections, 1 equation, 2 figures, 6 tables, 2 algorithms)

This paper contains 23 sections, 1 equation, 2 figures, 6 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Related Work
  3. SAT and Arithmetic Verification
  4. Clause Management of Modern SAT Solvers
  5. Methodology
  6. Overview of the Proposed Algorithm
  7. Stage 1: Dynamic Usage Filtering
  8. Stage 2: Lineage-Oriented Selection
  9. Reduction Triggering Policy and Amount
  10. Reduction Triggering Policy
  11. Reduction Percentage
  12. Experiments
  13. Implementation Details
  14. Datasets
  15. Setups and Metrics
  16. ...and 8 more sections

Figures (2)

  • Figure 1: Heatmap distributions of learnt clauses, correlating clause length (x-axis) with LBD (y-axis). For (a) LBD provides a rich and dynamic quality metric that is distinct from static clause length. For (b), the distribution collapses into a sharp diagonal line, indicating the LBD of a learnt clause is almost always consistent with its length. Therefore, LBD-based clause reduction heuristic fails to consider the dynamic behavior of variable decision beyond the static clause length already offers.
  • Figure 2: Comparison on Random 3-SAT Problems