Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Deeply Optimizing the SAT Solver for the IC3 Algorithm

Yuheng Su, Qiusong Yang, Yiwei Ci, Yingcheng Li, Tianjun Bu, Ziyu Huang

TL;DR

This paper targets the SAT-solving bottlenecks in IC3/PDR by introducing GipSAT, a purpose-built CDCL solver. It combines three core innovations: domain-restricted decision/propagation to minimize variable assignments, bucket-based VSIDS for constant-time updates, and reuse of a single activation variable to handle temporary clauses without solver resets. Empirical results on HWMCC benchmarks show GipSAT achieving an average solving-time speedup of $3.61\times$ over Minisat and solving $23$ more cases, substantially improving IC3 scalability. The work suggests GipSAT as a practical route to faster IC3-based verification and motivates future exploration into word-level SMT support for IC3.

Abstract

The IC3 algorithm, also known as PDR, is a SAT-based model checking algorithm that has significantly influenced the field in recent years due to its efficiency, scalability, and completeness. It utilizes SAT solvers to solve a series of SAT queries associated with relative induction. In this paper, we introduce several optimizations for the SAT solver in IC3 based on our observations of the unique characteristics of these SAT queries. By observing that SAT queries do not necessarily require decisions on all variables, we compute a subset of variables that need to be decided before each solving process while ensuring that the result remains unaffected. Additionally, noting that the overhead of binary heap operations in VSIDS is non-negligible, we replace the binary heap with buckets to achieve constant-time operations. Furthermore, we support temporary clauses without the need to allocate a new activation variable for each solving process, thereby eliminating the need to reset solvers. We developed a novel lightweight CDCL SAT solver, GipSAT, which integrates these optimizations. A comprehensive evaluation highlights the performance improvements achieved by GipSAT. Specifically, the GipSAT-based IC3 demonstrates an average speedup of 3.61 times in solving time compared to the IC3 implementation based on MiniSat.

Deeply Optimizing the SAT Solver for the IC3 Algorithm

TL;DR

This paper targets the SAT-solving bottlenecks in IC3/PDR by introducing GipSAT, a purpose-built CDCL solver. It combines three core innovations: domain-restricted decision/propagation to minimize variable assignments, bucket-based VSIDS for constant-time updates, and reuse of a single activation variable to handle temporary clauses without solver resets. Empirical results on HWMCC benchmarks show GipSAT achieving an average solving-time speedup of over Minisat and solving more cases, substantially improving IC3 scalability. The work suggests GipSAT as a practical route to faster IC3-based verification and motivates future exploration into word-level SMT support for IC3.

Abstract

The IC3 algorithm, also known as PDR, is a SAT-based model checking algorithm that has significantly influenced the field in recent years due to its efficiency, scalability, and completeness. It utilizes SAT solvers to solve a series of SAT queries associated with relative induction. In this paper, we introduce several optimizations for the SAT solver in IC3 based on our observations of the unique characteristics of these SAT queries. By observing that SAT queries do not necessarily require decisions on all variables, we compute a subset of variables that need to be decided before each solving process while ensuring that the result remains unaffected. Additionally, noting that the overhead of binary heap operations in VSIDS is non-negligible, we replace the binary heap with buckets to achieve constant-time operations. Furthermore, we support temporary clauses without the need to allocate a new activation variable for each solving process, thereby eliminating the need to reset solvers. We developed a novel lightweight CDCL SAT solver, GipSAT, which integrates these optimizations. A comprehensive evaluation highlights the performance improvements achieved by GipSAT. Specifically, the GipSAT-based IC3 demonstrates an average speedup of 3.61 times in solving time compared to the IC3 implementation based on MiniSat.

Paper Structure

This paper contains 18 sections, 1 theorem, 4 figures, 3 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Basics and Notations
  4. Incremental CDCL SAT Solver
  5. IC3 Algorithm
  6. Motivations
  7. Optimizations
  8. Decide and Propagate in Domain
  9. VSIDS by Bucket
  10. Without Resetting
  11. Implementation
  12. Evaluation
  13. Experiment Setup
  14. Experimental Results
  15. Analysis
  16. ...and 3 more sections

Key Result

theorem thmcountertheorem

To solve $Q_{relind}$ with a temporary clause $\mathbf{c}$ by utilizing the activation variable $\mathbf{a}$, we consider the formula: $\text{sat}(F_{i} \land (c \lor a) \land T \land \lnot c' \land \lnot a)$, where $\lnot c' \land \lnot a$ serves as the temporary assumption. If a learned clause $\m

Figures (4)

  • Figure 4: The number of cases solved by different SAT solvers over time.
  • Figure 5: The comparison of solving time(s) between GipSAT and other solvers in rIC3. Points above the gray solid line indicate that GipSAT performs better. The purple dashed line represents the geometric mean of the speedup.
  • Figure 6: The comparison of average solving time(s) for queries between GipSAT and Minisat in rIC3. Points below the gray diagonal indicate that GipSAT performs better.
  • Figure 7: The comparison of proof-obligation length, number of frames, and invariant size (safe instances) between GipSAT and Minisat in rIC3.

Theorems & Definitions (2)

  • theorem thmcountertheorem
  • proof