SMT sampling refers to the task of generating a set of satisfying assignments (samples) for a given SMT formula. An effective SMT sampler should be capable of producing samples with high diversity to maximize coverage of the solution space. However, most SMT samplers struggle to adequately cover the solution space and fail to generate sufficiently diverse solutions. To address these limitations, we propose \( HighDiv \) , the first iterative sampling framework that integrates CDCL(T) and local search in a bidirectional guided manner. During the bidirectional guidance process, solutions generated by CDCL(T) guide the variable initialization of the local search. Conversely, solutions produced by the local search guide CDCL(T) to further explore the solution space. Additionally, we design a novel local search algorithm, Context-Constrained Stochastic Search (CCSS), which introduces the Constraint-Partitioned Variable Initialization and the boundary-aware move operator. These components effectively balance exploration and feasibility throughout the search process. We conduct an extensive evaluation on QF_LIA formulas from the SMT-LIB benchmark. The results demonstrate that \( HighDiv \) achieves substantial improvements in diversity over the state-of-the-art SMT sampling tools.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

SMT(LIA) Sampling with High Diversity

  • Yong Lai,
  • Junjie Li,
  • Chuan Luo

摘要

SMT sampling refers to the task of generating a set of satisfying assignments (samples) for a given SMT formula. An effective SMT sampler should be capable of producing samples with high diversity to maximize coverage of the solution space. However, most SMT samplers struggle to adequately cover the solution space and fail to generate sufficiently diverse solutions. To address these limitations, we propose \( HighDiv \) , the first iterative sampling framework that integrates CDCL(T) and local search in a bidirectional guided manner. During the bidirectional guidance process, solutions generated by CDCL(T) guide the variable initialization of the local search. Conversely, solutions produced by the local search guide CDCL(T) to further explore the solution space. Additionally, we design a novel local search algorithm, Context-Constrained Stochastic Search (CCSS), which introduces the Constraint-Partitioned Variable Initialization and the boundary-aware move operator. These components effectively balance exploration and feasibility throughout the search process. We conduct an extensive evaluation on QF_LIA formulas from the SMT-LIB benchmark. The results demonstrate that \( HighDiv \) achieves substantial improvements in diversity over the state-of-the-art SMT sampling tools.