一句话：提出两层混合框架 HybridSMT，深度融合 CDCL(T) 与随机局部搜索求解 SMT(NIA)，显著提升求解性能。
问题：SMT(NIA) 在软件工程中应用广泛，主流框架为 CDCL(T)，随机局部搜索（SLS）亦被证明有效，但二者协作尚未被研究。方法：受 SAT 中 CDCL 与 SLS 深度合作成功的启发，提出两层混合方法：外层在内层与独立 SLS 求解器间交替；内层以 CDCL(T) 为主体，设计 DCL(T) 引导的 SLS 求解器，在对应骨架解的分支处调用，并向 CDCL(T) 返回信息以改进分支启发式。在 Z3 的 CDCL(T) tactic 与 LocalSMT 上实现，得到 HybridSMT。结果：在 SMT-LIB 标准基准（多来自终止性分析等真实应用）上，HybridSMT 显著提升 Z3 的 CDCL(T)，比当前最好的 SMT(NIA) 求解器多解 10.36% 实例，对软件验证实例更高效。
Satisfiability Modulo Theory (SMT) generalizes the propositional satisfiability problem (SAT) by extending support for various first-order background theories. In this paper, we focus on the SMT problems in Non-Linear Integer Arithmetic (NIA) theory, referred to as SMT(NIA), which has wide applications in software engineering. The dominant paradigm for SMT(NIA) is the CDCL(T) framework, while recently stochastic local search (SLS) has also shown its effectiveness. However, the cooperation between the two methods has not been studied yet. Motivated by the great success of the deep cooperation of CDCL and SLS for SAT, we propose a two-layer hybrid approach for SMT(NIA). The outer-layer interleaves between the inner-layer and an independent SLS solver. In the inner-layer, we take CDCL(T) as the main body, and design DCL(T)-guided SLS solver, which is invoked at branches corresponding to skeleton solutions and returns useful information to improve the branching heuristics of CDCL(T). We implement our ideas on top of the CDCL(T) tactic of Z3 with an SLS solver called LocalSMT, resulting in a hybrid solver dubbed HybridSMT. Extensive experiments are carried out on the standard SMT(NIA) benchmarks from SMT-LIB, where most of the instances are from real-world software engineering applications of termination and non-termination analysis. Experiment results show that HybridSMT significantly improves the CDCL(T) solver in Z3. Moreover, our solver can solve 10.36% more instances than the currently best SMT(NIA) solver, and is more efficient for software verification instances.
DOI 原文 ·
@inproceedings{paperbot11319,
title = {Deep Combination of CDCL(T) and Local Search for Satisfiability Modulo Non-Linear Integer Arithmetic Theory},
author = {Xindi Zhang and Bohan Li and Shaowei Cai},
booktitle = {ICSE},
year = {2024},
doi = {10.1145/3597503.3639105}
}