摘要：
本次报告将以可满足性问题为中心，包括命题可满足性问题（SAT）、可满足性模理论（SMT）以及求解算法等，通过一系列自动推理与深度学习交叉的工作，探讨深度学习在自动推理和约束求解领域的定位与意义。作为计算机领域的根本性问题，可满足性问题在模型检测、硬件和软件形式化验证、数学证明和推理等广泛应用中发挥着重要作用。随着深度学习的快速发展，它为可满足性算法中专家策略等的设计提供了重要的参考，为求解复杂问题提供了新的思路和方法。当前，将深度学习与可满足性求解算法相结合的研究也成为自动推理领域的重要前沿方向。

报告人简介：
贾富琦，目前就读于中国科学院大学，2020级博士研究生。其研究方向包括自动推理、约束求解、神经符号方法，具体方向为SAT/SMT求解算法研究、深度学习与自动推理的交叉研究。研究成果发表于NeurIPS, AAAI, ISSTA, ASE等国际会议，并获得了2023年ACM Sigsoft杰出论文奖。目前独立开发的SMT求解器支持非线性整数理论，在SMT-COMP中取得了Single Query和Model Validation Track的第二名的成绩。

讨论班简介：北京大学应用数学青年讨论班 (Applied Mathematics Seminar for Youth) 是一个由北京大学卓越研究生计划组织的学术交流平台。该讨论班定期举办一系列读书会、学术报告，涵盖广泛的应用数学领域，旨在为应用数学领域的学生提供一个互相学习、交流和探讨的机会，促进学生们在该领域的学术成长和思维能力的培养。

报名问卷：需要预定午餐的老师同学请填报名问卷 https://wj.qq.com/s2/13199304/a37a/

（由于需要提前预订午餐，请感兴趣参会的老师和同学在9月28号9点之前填写问卷，谢谢！）