Deeply Optimizing the SAT Solver for the IC3 Algorithm

TL;DR

This paper presents a set of targeted optimizations for the SAT solver used in the IC3 model checking algorithm, leading to significant performance improvements with a new lightweight solver, GipSAT.

Contribution

The paper introduces novel optimizations tailored for IC3's SAT queries and develops GipSAT, a lightweight solver that outperforms MiniSat-based IC3 in speed.

Findings

GipSAT achieves an average 3.61x speedup over MiniSat-based IC3.

Optimizations include variable subset computation, bucket-based VSIDS, and efficient clause management.

GipSAT significantly enhances the efficiency of the IC3 model checking process.

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.