Junjie Li

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 SMTLIB benchmark. The results demonstrate that HighDiv achieves substantial improvements in diversity over the state-of-the-art SMT sampling tools.