2021年7月10日，正在巴塞罗那举办的国际SAT竞赛组委会学术年会公布了2021年度第24届国际SAT竞赛结果，金沙威尼斯官网金沙威尼斯欢乐娱人城系统可信性自动验证国家地方联合工程实验室徐扬教授团队取得优异成绩，李志辉副教授小组研发的求解器“Relaxed LCMDCBDL SCAVEL01”获得Crypto组第二名、吴贯锋老师小组研发的求解器“P-MCOMSPS-STR-32-SC”获得Parallel Track UNSAT组第三名。
SAT（可满足性，SATisfiability）问题是第一个被证明的NP完全问题，也是当今数学、计算机科学和人工智能等领域研究的前沿核心问题之一。许多重要领域中的大量问题，如大规模集成电路的自动布线及其正确性验证、软件自动开发及其正确性验证、机器人动作规划、大型数据库的维护以及包括财政、金融领域在内的许多优化问题等，都可转化为SAT问题求解。因此，致力于构建求解SAT问题的快速有效系统——SAT求解器这一基础性工具，不仅在理论研究上而且在应用领域都具有极其重要的意义。
国际SAT竞赛是学术界和工业界在SAT问题研究领域的最顶级赛事，每一到两年举办一次，至今已经举办了二十四届。本次竞赛设有Main、Crypto Track、Parallel Track、No-Limit Track、Cloud Track和CaDiCaL Hack Track共六个组，共有来自于16个国家的七十多个求解器参赛。参赛单位包括奥地利约翰尼斯开普勒大学、英国曼彻斯特大学、法国阿尔图瓦大学、中国中科院、中国西安电子科技大学、德国安全研究实验室，Intel，Google等世界各地的大学、研究机构及企业。竞赛题目均为业界实际应用问题转换而来，其中Crypto Track组竞赛题目200个基准测试样例，全部来自于密码破解问题。
相关链接：
第24届国际SAT竞赛主页：https://satcompetition.github.io/2021/
竞赛成绩公布文档：https://satcompetition.github.io/2021/slides/ISC2021.pdf
