求解器理论分析：理论算法与实验算法的碰撞丨CNCC

CCF杰出会员，中国科学院软件研究所研究员

CCF学术工委执行委员，中国科学院软件研究所研究员，中国科学院优秀导师，CCF杰出会员/学术工委执行委员，研究约束求解和形式化验证，获得领域相关顶级会议CAV、CP、SAT等会议的最佳/杰出论文奖，多次获得SAT比赛、SMT比赛和MaxSAT比赛冠军，担任SAT 2027会议程序委员会主席。其求解器应用于包括华为、华大九天、中国航空制造研究院、国家电网、阿里巴巴、微软等多家企业/机构在内的多个实际场景，包括集成电路验证、操作系统验证、云计算调度和航空制造调度等。

论坛共同主席

CCF杰出会员，上海财经大学教授

上海财经大学计算机与人工智能学院院长、计算经济交叉科学教育部重点实验室创始主任、理论计算机科学研究中心创始主任。主要研究理论计算机，并注重与其它学科的交叉，在理论计算机的三大会议STOC/FOCS/SODA共发表论文30+篇。荣获ICALP2007、FAW2010、ISAAC2010 等重要国际会议最佳论文奖。曾荣获ACM杰出科学家奖（2019）、第八届世界华人数学家大会ICCM数学奖（原晨兴数学奖）银奖（2019）、CCF青年科学家（2014）等荣誉。

论坛讲者

南京大学教授

南京大学教授、博士生导师。本科毕业于清华大学计算机科学与技术系，以及姚期智理论计算机科学实验班，于普林斯顿大学获得博士学位。研究方向为理论计算机科学领域、算法设计和组合优化。在若干经典和基础问题上做出了重大突破。研究成果获理论计算机科学一流会议ICALP 2011单独作者最优秀学生论文奖、旗舰会议FOCS 2012最佳论文奖、ICALP 2024最佳论文奖，成果发表于计算机科学领域的旗舰期刊 Journal of the ACM (JACM)。现担任国际期刊《Transactions on Algorithms》编委。

报告题目：The Use of Linear Programming in Approximation Algorithm Design

摘要：Many practical problems are NP-hard, yet we often need algorithms to solve them fast. Approximation algorithms offer a way to design efficient algorithms that provide solutions with provable guarantees. Over the past three decades, linear programming has become a powerful and widely used tool in designing such algorithms. In this talk, I will present several techniques for leveraging linear programming to develop approximation algorithms for NP-hard problems.

上海交通大学教授

上海交通大学计算机系教授。于上海交通大学获得软件与理论专业博士、于德国弗莱堡大学获得数学博士。主要研究兴趣为计算机与数学的交叉领域，包括逻辑、算法与计算复杂性。目前担任《Logic Methods in Computer Science》和《Theory of Computing Systems》两本国际期刊编委。

报告题目：Constructing hard instances for SAT and beyond

摘要：Assuming P≠NP, every algorithm A deciding SAT has a sequence of hard instances, i.e., A runs in super-polynomial time on these instances. Polynomial-time construction of such a sequence amounts to improving the algorithm A. In this talk, I will discuss a proof-theoretic approach to this problem, particularly under the assumption that the class TAUT of tautologies of propositional logic has no p-optimal proof system. We will also discuss the extension of this result to every πtp-complete problem with t≥1 in the polynomial hierarchy.

中国科学院数学与系统科学研究院工程师

主要研究方向为混合整数规划算法、软件及其应用，是国产混合整数规划软件CMIP的创始骨干成员。主持国家自然科学基金青年基金项目；入选中国科学院技术人才支撑项目；获中国运筹学会青年人才发展专项；获中国运筹学会科学技术奖运筹应用奖；在运筹优化的著名刊物JOGO、EJOR等发表若干文章。与华为、阿里、电科院等企业以及国防单位合作，解决了许多实际应用中的优化问题。

报告题目：混合整数规划求解器发展与思考

摘要：混合整数规划（Mixed Integer Programming, MIP）广泛应用于各个领域。近几年MIP国产求解器蓬勃发展的同时，随着应用领域的深入与扩展，更复杂、更具挑战性的现实需求不断涌现。由于MIP问题固有的NP难特性，其求解过程极易遭遇性能瓶颈，这对求解器的核心能力提出了更高要求。本报告将讨论求解器如何更好地将MIP理论与求解器相结合，如何更好地将MIP求解器与实际应用相结合，分享一些自己的思考与挑战。

CCF杰出会员，华中科技大学教授

华中科技大学卓越学者计划特聘岗教授，智能科学与技术专业负责人，华中科技大学霍普克罗夫特计算科学研究中心执行主任，CCF杰出会员，2016年入选德国海德堡阿贝尔/菲尔兹/图灵奖基金会全球200名杰出青年学者。主要研究领域包括人工智能、深度学习、AI4Sci等。在领域内主流期刊和会议上发表了200余篇学术论文，入选2023、2024年全球前2%顶尖科学家榜单。曾获约束与规划国际学术会议CP 2021最佳论文奖、多次获SAT、MaxSAT竞赛冠军。

报告题目：MaxSAT局部搜索与完备算法的若干设计与思考

摘要：作为布尔可满足性问题（SAT）的优化形式，最大可满足性问题(MaxSAT)是具有NP难度的高复杂度问题。局部搜索是求解MaxSAT问题的一种有效且轻量级的方法，其核心模块包括初始化、变元选择、子句加权等。本报告将首先聚焦于MaxSAT局部搜索求解器的设计，涵盖了上述几大模块的求解策略与算法设计的思考。另外，分支限界（BnB）是设计组合优化问题完备求解器的强大工具，但在2021年以前一直在MaxSAT完备求解上表现不佳。本报告接下来将讨论如何通过结合子句学习和分支策略，设计相应的BnB MaxSAT完备求解器。最后，如何对MaxSAT的求解策略和行为表现进行理论分析、解释和指导，是可以进一步探讨的方向。