本课程为靠谱的网赌平台-安全靠谱的网赌平台大全 本研合上课程。
时间：2024年秋季学期，9月12日开始，双周二3-4节，每周四5-6节。
地点：三教206。
答疑：单周二10:00-11: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.
成绩判定：
本课程选课学生需要做一次关于前沿论文的课堂报告（可从2023年29th International Conference on Principles and Practice of Constraint Programming会议长文（序号6-41之间）中任选一篇进行报告），并完成一篇课程论文。期末成绩基于课堂报告水平和课程论文质量综合评定。
课程日程安排（具体上课日期及讲授内容可能会有所调整，以课程微信群通知为准）：
| 时间 | 内容 |
| 2024.9.12 | Lecture 1: Introduction to Constraint Programming and Constraint Satisfaction Problems |
| 2024.9.19 | Lecture 2: Constraint Programming in a Nutshell (I): CSP Examples & Equivalence of CSPs |
| 2024.9.26 | Lecture 3: Constraint Programming in a Nutshell (II): Basic Framework & Examples |
| 2024.10.10 | Lecture 4: Constraint Solvers (I) |
| 2024.10.15 | Lecture 5: Constraint Solvers (II) |
| 2024.10.17 | Lecture 6: Local Consistency (I) |
| 2024.10.24 | Lecture 7: Local Consistency (II) |
| 2024.10.29 | Lecture 8: Some Incomplete Constraint Solvers (I) |
| 2024.10.31 | Lecture 9: Some Incomplete Constraint Solvers (II) |
| 2024.11.7 | Lecture 10: Some Incomplete Constraint Solvers (III) |
| 2024.11.12 | Lecture 11: Some Incomplete Constraint Solvers (IV) & Constraint Propagation Algorithms (I) |
| 2024.11.14 | Lecture 12: Constraint Propogation Algorithms (II) |
| 2024.11.21 | Lecture 13: Search (I) |
| 2024.11.26 | Lecture 14: 面向关键系统软件的约束求解技术研究 |
| 2024.11.28 | Lecture 15: Search (II) and Some Further Issues in Constraint Programming |
| 2024.12.5（改至12.17） | 丁天仪：Towards More Efficient Local Search for Pseudo-Boolean Optimization 秦子瀚： Learning a Generic Value-Selection Heuristic Inside a Constraint Programming Solver 何宇航：Distribution Optimization in Constraint Programming 许飞龙：A CP Approach for the Liner Shipping Network Design Problem |
| 2024.12.10 | 仝佳驹：Incremental Constrained Clustering by Minimal Weighted Modification 岳关璋：Guiding Backtrack Search by Tracking Variables During Constraint Propagation 王秭如：Preprocessing in SAT-Based Multi-Objective Combinatorial Optimization 童雪飞： Fast Matrix Multiplication Without Tears: A Constraint Programming Approach |
| 2024.12.12 | 原梓轩：SAT-Based Learning of Compact Binary Decision Diagrams for Classification 李代波：Guided Bottom-Up Interactive Constraint Acquisition 黄安渝：Proof Logging for Smart Extensional Constraints 徐艺轩：Constraint Programming with External Worst-Case Traversal Time Analysis |
| 2024.12.19 | 林与心：An Efficient Constraint Programming Approach to Preemptive Job Shop Scheduling 李昌林：Symmetries for Cube-And-Conquer in Finite Model Finding 侯天尧：Addressing Problem Drift in UNHCR Fund Allocation 蒋穆清：Optimization Models for Pickup-And-Delivery Problems with Reconfigurable Capacities |
| 2024.12.24 | 贾梓涵：Using Canonical Codes to Efficiently Solve the Benzenoid Generation Problem with Constraint Programming 白亦璠：The p-Dispersion Problem with Distance Constraints 雷斐然：Exploring Hydrogen Supply/Demand Networks: Modeller and Domain Expert Views |
| 2024.12.26 | 杨雪巍：Exploiting Configurations of MaxSAT Solvers 陈家苇：Optimization of Short-Term Underground Mine Planning Using Constraint Programming 王一鸣：TBC |
课程论文可选题目：
1.
设计并实现K-framework[1]相应SMT证明生成方案。
2. 基于SMT对强化学习系统及环境进行形式化建模，在此基础上设计并实现强化学习系统的测试用例生成方案[2]。
3. 实现从Mediator语言[3]到Z3转换的工具实现，并设计相关实例利用Z3求解器对Mediator模型性质进行验证。
4. 结合符号执行与约束求解技术，对Algorand智能合约[4,5,6]进行形式化建模，并对其进行漏洞检测与分析。
5. 自己选择一种约束求解器，在其中对Stellar共识协议[7,8]或Giskard共识协议[9]进行形式化建模，并对其安全性、活性等性质进行验证。
6. 对当前国际上关于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] Yuteng Lu, Weidi Sun, and Meng Sun. Towards Mutation Testing of Reinforcement Learning Systems. Journal of Systems Architecture, vol. 131, 102701, 2022.
[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] David Mazieres. The stellar consensus protocol: A federated model for internet-level consensus.
Stellar Development Foundation, 2016.
[8] Giuliano Losa, Mike Dodds. On the Formal Verification of the Stellar Consensus Protocol. FMBC@CAV 2020: 9:1-9:9
[9] Elaine Li, Karl Palmskog, Mircea Sebe, Grigore Roşu. Specification of the Giskard Consensus Protocol. CoRR abs/2010.02124, 2020.
论文说明及要求：
1) 选题目1-5的同学可合作（选题目1-3同组合作者不超过3人，选题目4、5同组合作者不超过2人）或独立完成，选择题目6的同学需独立完成。
2) 选题目1-5的同学需同时提交完整代码（或将代码开源并提供代码链接）和论文。
3) 合作者需在课程论文后具体说明每人在工作（主要包括代码实现和论文写作）中的贡献分工。
4) 论文中英文均可。题目1-5中文软件学报格式正文（不含参考文献）12-15页（文中可包含核心代码，但所有代码长度总计不超过1页），英文LNCS格式正文（不含参考文献）16-20页（文中可包含核心代码，但所有代码长度总计不超过1页）。题目6综述论文中文软件学报格式正文（不含参考文献）25-30页，英文LNCS格式正文（不含参考文献）35-40页，参考文献不少于30篇。
5) 2024年12月15日之前通过教学网提交。