近日，软件所计算机科学国家重点实验室和并行软件与计算科学实验室研究团队的论文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（项目链接：https://github.com/MRVAPOR/BLAN）。相比于目前主流的SMT求解器，如：微软团队的Z3、斯坦福大学和爱荷华大学主导研发的CVC5等，BLAN在可满足实例求解的性能上有了显著提升。 

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

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

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

　　图一 获奖证书 

　　图二 BLAN求解器示意图 

　　图三 部分实验结果展示(求解时间-求解实例个数图)