报告题目：基于大模型的SAT求解器研发
报告人：蔡少伟
邀请人：李志辉
讲座时间：2025年12月18日（星期四）下午15:30-17:00
讲座地点：犀浦校区三号教学楼X30423
报告摘要：
布尔可满足性问题（SAT）是经典的NP完全问题。SAT求解器有重要的应用，但其研发有很高的门槛。近几年来，大模型技术展现了在复杂算法研发的能力，通过多智能体技术，其正确性和效果可以达到工业级应用的水平。本报告介绍基于大模型研发的SAT求解器，其性能达到前沿水平。
报告人简介：
蔡少伟，中国科学院软件研究所研究员，中国科学院优秀导师，CCF杰出会员/学术工委执行委员，研究约束求解和形式化验证，主持自然科学基金委青年B项目和重点项目，获得领域顶级会议CAV、CP、SAT等会议的最佳/杰出论文奖，多次获得SAT比赛、SMT比赛和MaxSAT比赛冠军，以及鸿蒙创新大赛冠军等，担任SAT会议程序委员会主席，受邀到SAT，CP，FMCAD等领域顶级会议做特邀报告。其求解器应用于包括华为、华大九天、中国航空集团、国家电网、阿里巴巴、微软等多家企业/机构在内的多个实际场景，包括集成电路验证、操作系统验证、云计算调度和航空制造调度等。
