arXiv cs.AI· Tianyi Ding, Haokun Li, Xinpeng Ni, Bican Xia, Tianqi Zhao·· 10 小时前AI 评分20
混合 SMT-NRA 求解器：融合 2D 单元跳跃局部搜索、MCSAT 与 OpenCAD
A Hybrid SMT-NRA Solver: Integrating 2D Cell-Jump-Based Local Search, MCSAT and OpenCAD
AI 导读
研究者提出一种 SMT-NRA 混合求解框架，将新设计的 2D-LS 局部搜索、MCSAT 与 OpenCAD 集成，通过信息交换提升搜索效率。其中 2D-cell-jump 将原有沿直线更新赋值的 cell-jump 推广到任意选定平面上的搜索。实验结果显示局部搜索性能有所提升。
正文 · AI 翻译
摘要：本文针对非线性实数算术理论的可满足性模理论（简称 SMT-NRA）提出了一种混合框架。首先，我们引入一种二维单元跳跃移动，称为 \emph{2D-cell-jump}，它推广了 SMT-NRA 局部搜索方法中的关键操作——单元跳跃。与现有仅沿给定直线更新赋值的单元跳跃不同，2D-cell-jump 能够在任意选定的平面上进行搜索。然后，我们提出了一种扩展的局部搜索框架，命名为 \emph{2D-LS}（沿用现有的 SMT-NRA 局部搜索框架 LS）。最后，我们提出了一种集成 2D-LS、MCSAT 和 OpenCAD 的 SMT-NRA 混合框架，通过信息交换提高搜索效率。实验结果表明局部搜索性能得到提升，凸显了所提方法的有效性。
| 评论： | SETTA 2026 的定稿版本 |
| 主题： | 人工智能（cs.AI）；计算机科学中的逻辑（cs.LO）；符号计算（cs.SC） |
| 引用为： | arXiv:2507.00557 [cs.AI] |
| （或 arXiv:2507.00557v3 [cs.AI] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2507.00557 由 DataCite 颁发的 arXiv DOI |
提交历史
来自：Tianyi Ding [查看电子邮件]
[v1]
2025年7月1日星期二 08:27:29 UTC（3,728 KB）
[v2]
2025年7月11日星期五 15:40:25 UTC（3,575 KB）
[v3]
2026年10月30日星期五 14:03:11 UTC（5,187 KB）
来源：arXiv cs.AI · arxiv.org