Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Revisiting Restarts of CDCL: Should the Search Information be Preserved?

Xindi Zhang, Zhihan Chen, Shaowei Cai

TL;DR

The paper investigates whether CDCL solvers should preserve search information across restarts and introduces cold restart policies that forget specific information. Through comprehensive experiments on leading solvers, it shows that forgetting the branching order ($FO$) or the phases ($FP$) generally yields improvements, while forgetting learnt clauses ($FC$) helps satisfiable instances but harms unsatisfiable ones; LBD-aware forgetting further refines this trade-off. The authors also present a parallel FO variant that delivers substantial speedups on satisfiable instances, highlighting the potential of memory-management heuristics to shape solver behavior. Overall, the work advocates a shift toward mixed exploitation-exploration restart strategies and dynamic information-management policies to build more satisfiable-oriented CDCL solvers.

Abstract

SAT solvers are indispensable in formal verification for hardware and software with many important applications. CDCL is the most widely used framework for modern SAT solvers, and restart is an essential technique of CDCL. When restarting, CDCL solvers cancel the current variable assignment while maintaining the branching order, variable phases, and learnt clauses. This type of restart is referred to as warm restart in this paper. Although different restart policies have been studied, there is no study on whether such information should be kept after restarts. This work addresses this question and finds some interesting observations. This paper indicates that under this popular warm restart scheme, there is a substantial variation in run-time with different randomized initial orders and phases, which motivates us to forget some learned information periodically to prevent being stuck in a disadvantageous search space. We propose a new type of restart called cold restart, which differs from previous restarts by forgetting some of the learned information. Experiments show that modern CDCL solvers can benefit from periodically conducting cold restarts. Based on the analysis of the cold-restart strategies, we develop a parallel SAT solver. Both the sequential and parallel versions of cold restart are more suitable for satisfiable instances, which suggests that existing CDCL heuristics for information management should be revised if one hopes to construct a satisfiable-oriented SAT solver.

Revisiting Restarts of CDCL: Should the Search Information be Preserved?

TL;DR

The paper investigates whether CDCL solvers should preserve search information across restarts and introduces cold restart policies that forget specific information. Through comprehensive experiments on leading solvers, it shows that forgetting the branching order () or the phases () generally yields improvements, while forgetting learnt clauses () helps satisfiable instances but harms unsatisfiable ones; LBD-aware forgetting further refines this trade-off. The authors also present a parallel FO variant that delivers substantial speedups on satisfiable instances, highlighting the potential of memory-management heuristics to shape solver behavior. Overall, the work advocates a shift toward mixed exploitation-exploration restart strategies and dynamic information-management policies to build more satisfiable-oriented CDCL solvers.

Abstract

SAT solvers are indispensable in formal verification for hardware and software with many important applications. CDCL is the most widely used framework for modern SAT solvers, and restart is an essential technique of CDCL. When restarting, CDCL solvers cancel the current variable assignment while maintaining the branching order, variable phases, and learnt clauses. This type of restart is referred to as warm restart in this paper. Although different restart policies have been studied, there is no study on whether such information should be kept after restarts. This work addresses this question and finds some interesting observations. This paper indicates that under this popular warm restart scheme, there is a substantial variation in run-time with different randomized initial orders and phases, which motivates us to forget some learned information periodically to prevent being stuck in a disadvantageous search space. We propose a new type of restart called cold restart, which differs from previous restarts by forgetting some of the learned information. Experiments show that modern CDCL solvers can benefit from periodically conducting cold restarts. Based on the analysis of the cold-restart strategies, we develop a parallel SAT solver. Both the sequential and parallel versions of cold restart are more suitable for satisfiable instances, which suggests that existing CDCL heuristics for information management should be revised if one hopes to construct a satisfiable-oriented SAT solver.
Paper Structure (18 sections, 2 figures, 7 tables)

This paper contains 18 sections, 2 figures, 7 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Background Knowledge
  4. Experimental Settings
  5. Run Time Variation with Warm Restarts
  6. Investigations on the Initial Order
  7. Investigations on the Initial Phases
  8. Evaluating Cold Restarts
  9. Forgetting the Branching Order
  10. Forgetting the Phases
  11. Forgetting Learnt Clauses
  12. LBD Threshold for Forgetting Learnt Clauses
  13. Learnt Clause Utilization
  14. Forgetting Multiple Types of Information
  15. Detailed Analysis for Preference
  16. ...and 3 more sections

Figures (2)

  • Figure 1: Runtime variations with different initial orders in log scale. The left (right) sub-figure reports the results of SAT (UNSAT) instances with circle (star) markers. The instances are sorted according to Kissat-MAB's run time, and we do not report the easy instances that can be solved by Kissat-MAB in less than 10 minutes.
  • Figure 2: Cumulative Distribution Function (CDF) for comparing our best sequential and parallel version with the best sequential and parallel competitor for the SAT and UNSAT instances of SC20 and SC21. The x-axis is the runtime in seconds, the y-axis is the number of solved instances. The higher the curve, the better the corresponding solver.