本课程为北京大学数学科学学院本研合上课程。
时间：2023年秋季学期，9月12日开始，单周二3-4节，每周四5-6节。
地点：三教106。
答疑：单周二14:00-15:00，也可邮件预约其他时间，理科楼1382。
课程内容：在学习了基本程序设计技术（计算概论），算法与数据结构的基本概念和技术的基础上，通过本课程进一步加强使用计算机解决问题的能力。约束编程、约束求解是近三十年来人工智能领域的一个重要研究方向，约束编程是一种声明式的编程范式，通过约束条件对变量之间的关系进行陈述，给出问题解的一些属性规范。课程中将讲解约束编程相关的技术与方法，所讲授的主要内容包括约束满足问题（CSP）、约束编程的基本框架、约束求解工具、一致性问题、约束传播及检索算法等内容，并对当前约束编程领域的新兴技术进行适当讨论。
教材及参考书目（[2,3]为数学学院图书馆馆藏）：
[1] Krzysztof Apt. Principles of Constraint Programming. Cambridge University Press, 2009.
[2] Francesca Rossi，Peter van Beek，Toby Walsh. Handbook of Constraint Programming. Elsevier, 2006.
[3] Thom Frühwirth, Slim Abdennadher. Essentials of Constraint Programming. Springer, 2003.
成绩判定：
本课程选课学生需要做一次关于前沿论文的课堂报告（可从2022年28th International Conference on Principles and Practice of Constraint Programming会议长文中任选一篇进行报告），并完成一篇课程论文。期末成绩基于课堂表现、报告水平和课程论文质量综合评定。
课程日程安排（具体上课日期及讲授内容可能会有所调整，以课程教学网通知为准）：
| 时间 | 内容 | 课件 |
| 2023.9.12 | Lecture 1: Introduction to Constraint Programming and Constraint Satisfaction Problems |
|
| 2023.9.14 | Lecture 2: Constraint Programming in a Nutshell (I): CSP Examples & Equivalence of CSPs |
|
| 2023.9.21 | Lecture 3: Constraint Programming in a Nutshell (II): Basic Framework & Examples |
|
| 2023.9.26 | Lecture 4: Constraint Solvers (I) |
|
| 2023.9.28 | Lecture 5: Constraint Solvers (II) |
|
| 2023.10.10 | Lecture 6: Constraint Solvers (III) & Local Consistency (I) |
|
| 2023.10.12 | Lecture 7: Local Consistency (II) |
|
| 2023.10.19 | Lecture 8: Some Incomplete Constraint Solvers (I) |
|
| 2023.10.24 | Lecture 9: Some Incomplete Constraint Solvers (II) |
|
| 2023.10.26 | Lecture 10: Some Incomplete Constraint Solvers (III) |
|
| 2023.11.2 | 开会停课一次，补课时间另行安排 |
|
| 2023.11.7 | Lecture 11: Some Incomplete Constraint Solvers (IV) & Constraint Propagation Algorithms (I) |
|
| 2023.11.9 | 开会停课一次，补课时间另行安排 |
|
| 2023.11.16 | Lecture 12: SMT公式的求解与解计数 |
|
| 2023.11.21 | Lecture 13: Constraint Propogation Algorithms (II) |
|
| 2023.11.23 | Lecture 14: Search (I) |
|
| 2023.11.28 | 补课：Lecture 15: Search (II), Lecture 16: Some Further Issues in Constraint Programming |
|
| 2023.11.30 | Lecture 17: Interactions as Constraints |
|
| 2023.12.5 | 王九同 汪济州 |
|
| 2023.12.7 | 刘梓豪 王一宁 史若虞 赵云潇 |
|
| 2023.12.14 | 冉佳鑫 陈林 马冰妤 艾一夫 |
|
| 2023.12.19 | 卢天泽 张书齐 杨宇轩 |
|
| 2023.12.21 | 郭尧昱 张杨 Embla Rán |
|
| 2023.12.28 | 覃烨成 操熙霖 朱梦才 胡适宇 |
课程论文可选题目：
1. 选择适当的约束求解器，在其中对神经网络公平性保障框架[1]给出完整的定义和实现，并设计相关实例进行验证。
2. 设计并实现K-framework[2]相应SMT证明生成方案。
3. 基于CSP对强化学习系统及环境进行形式化建模，在此基础上设计并实现强化学习系统的测试用例生成方案[3]。
4. 实现从Mediator语言[4]到Z3转换的工具实现，并设计相关实例利用Z3求解器对Mediator模型性质进行验证。
5. 选取某种约束求解器，在其中给出概率连接件关系模型[5]的实现，并对相关性质进行验证。
6. 对当前国际上基于SAT、LP、MILP、SMT等约束求解技术对神经网络进行验证的方法进行调研与比较，写一篇综述论文。
[1] Elias Benussi, Andrea Patane, Matthew Wicker, Luca Laurenti and Marta Kwiatkowska. Individual Fairness Guarantees for Neural Networks. Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence，pages 651-658, 2022.
[2] Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh, and Grigore Roşu. Towards a Trustworthy Semantics-Based Language Framework via Proof Generation. Proceedings of CAV 2021, LNCS 12760, pages 477-499, 2021.
[3] Yuteng Lu, Weidi Sun, and Meng Sun. Towards Mutation Testing of Reinforcement Learning Systems. Journal of Systems Architecture, vol. 131, 102701, 2022.
[4] Yi Li, Weidi Sun and Meng Sun. Mediator: A Component-based Modeling Language for Concurrent and Distributed Systems. Science of Computer Programming. vol. 192, 102438, 2020.
[5] Meng Sun and Xiyue Zhang. A Relational Model for Probabilistic Connectors Based on Timed Data Distribution Streams. in Proceedings of FORMATS 2018, LNCS 11022, pages 125-141, Springer, 2018.
论文要求：
1) 选题目1、2、3、4的同学可合作（同组合作者不超过2人）或独立完成，选择题目5、6的同学需独立完成。
2) 选题目1-5的同学需同时提交代码（或将代码开源并提供代码链接）和论文。
3) 合作者需在课程论文后具体说明每人在工作（主要包括代码实现和论文写作）中的贡献分工。
4) 题目1-5的论文中英文均可，中文软件学报格式正文（不含参考文献）不少于12页，英文LNCS格式正文（不含参考文献）不少于16页；题目6的论文需为英文，LNCS格式正文（不含参考文献）不少于20页，参考文献数不少于30篇，其中2023年参考文献不少于10篇。
5) 12月15日之前通过教学网提交。
综述论文示例：
[a] Ferdinando Fioretto, Enrico Pontelli, William Yeoh. Distributed Constraint Optimization Problems and Applications: A Survey. Journal of Artificial Intelligence Research, vol. 61, pages 623-698, 2018.
[b] Lucas Bordeaux, Youssef Hamadi, Lintao Zhang. Propositional Satisfiability and Constraint Programming: A comparative survey. ACM Computing Surveys, vol. 38(4), 12:1-12:54, 2006.
[c] Joxan Jaffar, Michael J. Maher. Constraint Logic Programming: A Survey. Journal of Logic Programming, vol. 19/20, pages 503-581, 1994.