SQuARE 组非线性整数约束求解研究工作获 ACM SIGSOFT 杰出论文奖

近日，SQuARE 组博士生贾富琦、马菲菲研究员和张健研究员，与中国科学院软件研究所计算机科学国家重点实验室、并行软件与计算科学实验室合作完成的论文《Improving Bit-Blasting for Nonlinear Integer Constraints》被软件工程领域顶级国际会议 ISSTA（International Symposium on Software Testing and Analysis）接收，并荣获 ACM SIGSOFT 杰出论文奖（ACM SIGSOFT Distinguished Paper Award）。

该论文针对非线性整数约束的求解，提出了一种基于位展开（Bit-Blasting）方法的求解框架，涵盖了搜索空间的预处理和位展开最优加和顺序的算法。团队自主研发并实现了 SMT 求解器 BLAN，在可满足实例求解性能上显著优于目前主流 SMT 求解器（如微软的 Z3、斯坦福与爱荷华大学的 CVC5 等）。

可满足性模理论 (SMT) 是自动推理的一个重要领域，它研究在某些特定理论（如：算术理论、数组理论等）下的一阶逻辑公式的可满足性的判定方法。而非线性整数约束则是其中一类常见且困难的约束类型，常出现在规划、软件 / 硬件验证和分析、自动化测试等实际问题中。在 SMT 中，一类经典的方法是通过位展开 (Bit-Blasting) 将非线性整数约束转化为对应的布尔可满足性问题进行求解。

通过观察和实践，团队发现目前主流的算法设计存在着诸多问题。针对这个现状，论文提出了一系列优化策略，显著提升了求解效率。针对搜索域难以确定的问题，论文提出了应对非线性乘法和特定约束的确定位长的启发式策略，以寻找到合适的搜索空间。针对连续加法中不同顺序导致冗余的问题，论文提出了一个最优顺序决策算法并证明了其最优性。详细的消融实验验证了所提方法的有效性。

此外，团队还进一步探究了位展开方法求解不可满足实例的实现路径。