针对IC3算法优化SAT求解器，速度提升3.6倍
Deeply Optimizing the SAT Solver for the IC3 Algorithm
- 仅决策必要变量，减少无谓计算
- 用桶替代堆，常数时间更新变量优先级
- 支持临时子句，避免频繁重置求解器
IC3算法（又称PDR）是一种基于SAT的模型检测方法，因其高效、可扩展和完备性近年来影响深远。它通过调用SAT求解器解决一系列与相对归纳相关的SAT查询。本文针对这些查询的独特特征提出多项优化：观察到并非所有变量都需在每次求解中决策，因此预先计算出必须决策的变量子集，确保结果不变；注意到VSIDS中二叉堆操作开销显著，改用桶结构实现常数时间操作；此外，支持临时子句而无需为每次求解分配新激活变量，从而避免求解器重置。我们开发了新型轻量级CDCL SAT求解器GipSAT，集成上述优化。全面评估表明，基于GipSAT的IC3相比基于MiniSat的实现，平均求解时间提速3.61倍。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。