可满足性模理论中的算术理论问题

可满足性模理论问题(简称SMT)是特点理论背景下的一阶逻辑公式可满足性问题，目前Z3，CVC5等主流SMT求解器已经成为了软件分析验证等领域的重要工具。 然而目前主流求解器均为完备方法，局部搜索算法作为一种高效的不完备求解方法，在SMT领域的尝试极少。我们设计了首个算术理论SMT问题的局部搜索求解器，名为LocalSMT，该求解器弥补了这一研究领域的空白，开创并引领这一研究方向。其突破了传统的求解框架, 在各类算术理论的算例集中,均达到了世界领先水平。针对算术理论,我们创新地设计了运算符及评分函数,使LocalSMT能够广泛地支持一系列算术理论：包括线性/非线性整数运算(LIA，NIA)，线性/非线性实数运算(LRA,NRA)。

此外，我们将LocalSMT与完备算法进行了深度融合，开发了混合求解技术，充分利用了两者性能互补的特点，大幅超过了当前的其他领先求解器。基于该混合技术开发的衍生求解器Z3++，在2021-2023年的SMT国际比赛中多次夺冠，并于2023年包揽了整数算术理论所有冠军。

最后，LocalSMT还被定制化适配，应用于页面自适应布局领域，用于App实时布局计算。目前求解性能已经达到毫秒级的实时响应，可用于手机终端的页面实时自动生成。该项目获得华为鸿蒙创新大赛一等奖。