7月13日，国际SAT竞赛组委会在其官方网站上公布了2018年SAT竞赛结果，我校数学学院，系统可信性自动验证国家地方联合工程实验室徐扬教授团队提交的求解器获得Main组亚军（比冠军Intel求解器的求解结果仅差0.75%），取得我校在该领域的历史性突破。

SAT（可满足性，SATisfiability）问题是第一个被证明的NP完全问题，也是当今数学、计算机科学和人工智能等领域研究的前沿核心问题之一。许多重要领域中的大量问题，如大型数据库的维护、大规模集成电路的自动布线及其正确性验证、软件自动开发及其正确性验证、机器人动作规划，数学中的许多优化问题等，都可转化为SAT问题求解。因此，致力于构建求解SAT问题的快速有效系统——SAT求解器这一基础性工具，不仅在理论研究上而且在许多应用领域都具有极其重要的意义。

国际SAT竞赛是学术界和工业界在SAT问题研究领域的最顶级赛事，每一到两年举办一次，至今已经举办了二十一届。本次竞赛共有来自于9个国家的41个求解器参赛。参赛单位包括英国曼彻斯特大学、法国阿尔图瓦大学、日本九州大学、德国卡尔斯鲁厄理工学院、中国西南交通大学、中国华中科技大学、德国安全研究实验室，Intel，Google等世界各地的大学、研究机构及企业。本次竞赛设有Main、Glucose Hack、NoLimith和Random四个组，

Main组是其中竞争最激烈的，竞赛题目均为工业界实际应用问题转换而来，因此其受到业界关注也是最多的。

徐扬教授团队在基于逻辑的自动推理相关研究领域工作多年，我校此次参赛的这类求解器已求解SAT问题24亿1700多万个，其中规模最大的有3.13万亿个文字（相当于有3.13万个逻辑电路器件），并基于这类求解器研发了Scavel系列的C程序、PLC程序自动验证工具，已广泛应用于航空航天、轨道交通、武器装备、信息安全、家用电子等领域。我校参加今年SAT竞赛团队主要成员包括徐扬教授、陈青山博士、吴贯锋博士等系统可信性自动验证国家地方联合工程实验室的多名教师和研究生。

                                                                   (数学学院供稿 撰稿 顾播雨)