7月8日，在意大利阿尔盖罗结束的第26届可满足性测试理论与应用国际会议(The 26th International Conference on Theory and Applications of Satisfiability Testing)中，我校数学学院系统可信性自动验证国家地方联合工程实验室徐扬教授团队取得优异成绩，李志辉副教授小组研发的求解器“CaDiCaL-Scave”获得Main组第二名。
可满足性测试理论与应用国际会议(SAT)是专注于命题可满足性问题的理论与应用的研究人员的顶级年度会议, 每一到两年举办一次，至今已经举办了二十六届。SAT（可满足性，SATisfiability）是当今数学、计算机科学和人工智能等领域研究的前沿核心问题之一。许多重要领域中的大量问题，如大规模集成电路的自动布线及其正确性验证、软件自动开发及其正确性验证、机器人动作规划、大型数据库的维护以及包括财政、金融领域在内的许多优化问题等，都可转化为SAT问题求解。在过去的二十年里，SAT研究的理论和实践的进步已经使SAT技术成为许多领域（包括在形式验证、人工智能、运筹学、计算生物学、密码学、数据挖掘、机器学习、数学等领域出现的问题）不可或缺的工具。因此，致力于构建求解SAT问题的快速有效系统——SAT求解器这一基础性工具，不仅在理论研究上而且在应用领域都具有极其重要的意义。
本年度SAT求解器国际竞赛共分为Main Track、Parallel Track、Cloud Track三个赛道。共有来自于26个国家的81个求解器参赛。参赛单位中国科学院软件研究所计算机科学国家重点实验室、中国科学院大学、华中科技大学、上海交通大学、美国卡耐基梅隆大学、奥地利林茨大学、德国德累斯顿大学、弗莱堡大学、卡尔斯鲁厄理工学院、加拿大滑铁卢大学、荷兰埃因霍温理工大学、法国皮卡第儒勒·凡尔纳大学、索邦大学、丹麦哥本哈根大学、瑞典隆德大学、印度理工学院、喀麦隆德尚大学、华为技术有限公司2012实验室、日本国家信息学研究所、德国理论信息学研究所等世界各地的大学、研究机构及企业。
我校系统可信性自动验证国地实验室徐扬教授团队长期致力于基于逻辑的自动演绎推理相关领域研究，原创地提出了基于矛盾体分离的多元、协同、动态自动演绎推理理论与方法。此次实验室组织了包括数学、计算机、电气在内的跨学科团队，结合多领域研究问题的形式化样例特征，进行多轮研讨推出了最新的求解器参赛。
相关链接：
第26届国际SAT竞赛主页：https://satcompetition.github.io/2023/index.html
竞赛成绩公布文档：
https://satcompetition.github.io/2023/downloads/satcomp23slides.pdf
