SMT(NRA)高效求解：结合局部搜索，MCSAT和openCAD的混合方法

报告摘要: 本报告围绕非线性实数算术的可满足性问题（SMT-NRA），介绍我们在多项式公式求解与局部搜索方法方面的最新研究进展。我们首先提出了一种面向仅包含严格不等式的 SMT-NRA 子类的局部搜索算法。该算法基于实根隔离，设计了一种名为 Cell-Jump 的新型跳跃操作，可沿指定方向跨越由多项式集合在实数空间中划分的胞腔（cell），从而实现原生支持非线性实数算术的局部搜索策略。 在此基础上，我们进一步提出了 二维 Cell-Jump（2D Cell-Jump） 操作，增强搜索的空间跳跃能力，并据此构建了局部搜索框架 2d-LS。为提升求解效率，我们将该框架与模型构造型可满足性演算（MCSAT）相结合，并引入 Sample-Cell 投影算子，用于在实数域中引导搜索避开冲突状态。最终，我们设计了一个融合 2d-LS、MCSAT 与 OpenCAD 的混合求解框架，通过信息交互进一步提升整体性能。实验结果表明，该方法在搜索效率和求解能力方面均取得了显著提升。

报告人简介: 李昊坤，2022年获北京大学博士学位，现于华为2012可信费马实验室形式化方法专家，参与多个重要的形式化验证项目。主要研究方向为符号计算，定理证明及程序验证，相关工作发表在CAV，ACL, ISSAC，JSC等国际知名期刊和会议上。