本课程为北京大学数学科学学院本研合上课程。

时间：2025年秋季学期，9月9日开始，单周二7-8节，每周四5-6节。

地点：一教202。

答疑：双周二15:00-17:00，智华楼353，需提前至少一天邮件预约，也可预约其他时间。

课程内容：在学习了基本程序设计技术（计算概论），算法与数据结构的基本概念和技术的基础上，通过本课程进一步加强使用计算机解决问题的能力。约束编程、约束求解是近三十年来人工智能领域的一个重要研究方向，约束编程是一种声明式的编程范式，通过约束条件对变量之间的关系进行陈述，给出问题解的一些属性规范，通过约束传播等算法对其进行求解。课程中将讲解约束编程相关的技术与方法，所讲授的主要内容包括约束满足问题（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.

成绩判定：

本课程选课学生需要做一次关于前沿论文的课堂报告（可从2024年30th International Conference on Principles and Practice of Constraint Programming会议长文（序号3-33之间）和2025年31th International Conference on Principles and Practice of Constraint Programming会议长文（序号3-40之间）中任选一篇进行报告），并完成一篇课程论文。期末成绩基于课堂报告水平和课程论文质量综合评定。

课程日程安排（第一次上课会建课程微信群，具体上课日期及讲授内容可能会有所调整，以课程微信群通知为准）：

课程论文可选题目：

1. 设计并实现K-framework[1]相应SMT证明生成方案。
2. 参考[2]的工作在大语言模型中结合SMT求解器提升大语言模型的可信性，在相关数据集上的实验表现至少需和[2]的结果持平或优于[2]的结果。
3. 实现从Mediator语言[3]到Z3转换的工具实现，并利用Z3求解器对不少于2个Mediator模型相关实例的性质进行验证。
4. 结合符号执行与约束求解技术，对Algorand智能合约[4,5,6]进行形式化建模，并对其进行漏洞检测与分析。
5. 自己选择一种约束求解器（不是用模型检查器），在其中对CKB共识协议[7]或Giskard共识协议[8]进行形式化建模，并对其安全性、活性等性质进行验证。
6. 参考[9]的工作，使用Z3给出[10]中连接件测试用例生成方法的实现。
7. 对当前国际上关于SMT求解技术在程序验证领域中的应用（循环不变式生成、程序终止性证明、模型检测、定理证明、插值计算、并发程序验证等）进行调研与比较，写一篇综述论文。

[1] 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.
[2] Shujie Deng, Honghua Dong, and Xujie Si. Enhancing and evaluating logical reasoning abilities of large language models. In ICLR 2024 Workshop on Secure and Trustworthy Large Language Models, 2024.
[3] 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.
[4] Zhiyuan Sun, Xiapu Luo, Yinqian Zhang. Panda: Security Analysis of Algorand Smart Contracts. USENIX Security Symposium, pages 1811-1828, 2023.
[5] Massimo Bartoletti, Andrea Bracciali, Cristian Lepore, Alceste Scalas, Roberto Zunino. A Formal Model of Algorand Smart Contracts. Financial Cryptography (1), LNCS vol. 12674, pages 93-114, 2021.
[6] Jing Chen, Silvio Micali. Algorand: A secure and efficient distributed ledger. Theoretical Computer Science, vol. 777, pages 155-183, 2019.
[7] Meng Sun, Yuteng Lu, Yi-chun Feng, Qi Zhang and Shaoying Liu. Modeling and Verifying the CKB Blockchain Consensus Protocol. Mathematics, vol. 9(22), 2954, 2021.
[8] Elaine Li, Karl Palmskog, Mircea Sebe, Grigore Roşu. Specification of the Giskard Consensus Protocol. CoRR abs/2010.02124, 2020.
[9] Xiyue Zhang, Weijiang Hong, Yi Li and Meng Sun. Reasoning about Connectors Using Coq and Z3. Science of Computer Programming, vol. 170, pages 27-44, 2019.
[10] Sun Meng，Farhad Arbab, Bernhard K. Aichernig, Lacramioara Astefanoaei, Frank S. de Boer and Jan Rutten. Connectors as Designs: Modeling, Refinement and Test Case Generation. In Science of Computer Programming. vol. 77(7-8), pages 799-822, 2012.

论文说明及要求：
1) 选题目1-6的同学可合作（选题目1-2同组合作者不超过3人，选题目3-6同组合作者不超过2人）或独立完成，选择题目7的同学需独立完成。
2) 选题目1-6的同学需同时提交完整代码（或将代码开源并提供代码链接）和论文。
3) 合作者需在课程论文后具体说明每人在工作（主要包括代码实现和论文写作）中的贡献分工。
4) 论文中英文均可。题目1-6中文软件学报格式正文（不含参考文献）12-15页（文中可包含核心代码，但所有代码长度总计不超过1页），英文LNCS格式正文（不含参考文献）16-20页（文中可包含核心代码，但所有代码长度总计不超过1页）。题目6综述论文中文软件学报格式正文（不含参考文献）25-30页，英文LNCS格式正文（不含参考文献）35-40页，参考文献不少于30篇。
5) 2025年12月21日之前通过教学网提交（不延期）。
6) 题目7的综述论文不得抄袭及使用AI工具自动生成，一经发现，本课程成绩为0。