一种混合 SMT-NRA 求解器：集成 2D 单元跳动局部搜索、MCSAT 与 OpenCAD
人工智能
2025-07-14 v2 计算机科学中的逻辑
符号计算
摘要
本文提出一种满足非线性实数算术 (SMT-NRA) 的混合框架。首先，我们引入一种二维单元跳动操作，称为 2d-cell-jump，概括了 SMT-NRA 局部搜索方法中的关键操作 cell-jump。随后，我们提出扩展的局部搜索框架，称为 2d-LS (遵循 SMT-NRA 的局部搜索框架 LS)，将模型构造满足术语 (MCSAT) 框架集成以提高搜索效率。为进一步提高 MCSAT 的效率，我们实现一种最近提出的技术，称为 sample-cell 投影算子，适用于 CDCL 风格的实数域搜索，有助于引导搜索远离冲突状态。最后，我们present一种集成 MCSAT、2d-LS 和 OpenCAD 的混合框架，用于通过信息交换提高搜索效率。实验结果表明，我们的方法在局部搜索性能方面取得了改进，凸显了所提出方法的有效性。
引用
@article{arxiv.2507.00557,
title = {A Hybrid SMT-NRA Solver: Integrating 2D Cell-Jump-Based Local Search, MCSAT and OpenCAD},
author = {Tianyi Ding and Haokun Li and Xinpeng Ni and Bican Xia and Tianqi Zhao},
journal= {arXiv preprint arXiv:2507.00557},
year = {2025}
}