课程号： 00135040
课程名称：程序设计技术与方法
开课学期：秋
学分： 3
先修课程：计算概论，数据结构与算法
基本目的：在学习了基本程序设计技术（计算概论），算法与数据结构的基本概念和技术的基础上，通过本课程进一步加强学生的程序设计能力和使用计算机解决问题的能力。约束编程、约束求解是近三十年来人工智能领域的一个重要研究方向，约束编程是一种声明式的编程范式，通过约束条件对变量之间的关系进行陈述，给出问题解的一些属性规范，并设计算法进行问题求解。课程中将讲解约束编程相关的技术与方法，所讲授的主要内容包括约束满足问题（CSP）、约束编程的基本框架、约束求解工具、一致性问题、约束传播及检索算法等内容，并对当前的新兴技术进行适当介绍。
内容提要：
- 概论（2学时） 约束编程基本概念，约束编程应用。
- 约束满足问题（4学时）约束满足问题的基本概念，整数域、实数域上的约束满足问题，布尔约束满足问题，符号约束满足问题，约束优化问题
- 约束编程基本框架（4学时）约束满足问题的等价性，约束求解过程，约束传播，布尔约束，整数区间上的多项式约束
- 完备约束求解器（4学时） 证明规则与证明系统的基本概念，UNIF证明系统，Martelli-Montanari算法，线性方程，Gauss-Jordan消去算法，Gaussian消去算法，实数上的线性不等式，Fourier-Motzkin消去算法
- 局部一致性（4学时）结点一致性，弧一致性，超弧一致性，有向弧一致性，路径一致性，有向路径一致性，k一致性，强k一致性，关系一致性，图与约束满足问题
- 不完备约束求解器（6学时） 等式及不等式约束，布尔约束，变换规则，域消减规则，整数区间上的线性约束，整数区间上的算术约束，实数域上的算术约束，实数域上的算术约束和方程
- 约束传播算法（4学时）一般循环算法，从偏序到约束满足问题，结点一致约束传播算法，弧一致约束传播算法，超弧一致约束传播算法，有向弧一致约束传播算法，路径一致约束传播算法，有向路径一致约束传播算法，k一致约束传播算法，强k一致约束传播算法，关系一致约束传播算法，不完备约束求解器的实现
- 检索算法（4学时）检索树，标记树，标记树上的检索算法，回溯法，分支限界法，启发式方法
- 约束编程语言及建模（4学时）变量、约束与表示法的选择，约束编程语言，约束传播，约束求解器，检索方法
- 新兴技术介绍与讨论（12学时） 神经网络验证、不变式合成、SMT问题等
教学方式：讲堂讲授+讨论，每周3学时
教材与参考书：
- Harold Abelson,Gerald Jay Sussman,Julie Sussman，Structure and Interpretation of Computer Programs, MIT。中译本《计算机程序的构造与解释》，机械工业出版社。
- Krzysztof Apt. Principles of Constraint Programming. Cambridge University Press, 2003.
- Francesca Rossi，Peter van Beek，Toby Walsh. Handbook of Constraint Programming. Elsevier, 2006.
- Thom Frühwirth, Slim Abdennadher. Essentials of Constraint Programming. Springer, 2003.
学生成绩评定方法：平时成绩10%，前沿研究报告40%，期末课程论文50%。
课程修订负责人：孙猛
