讲义-马菲菲-20201

【约束求解】是计算机科学和人工智能领域中的一个重要分支，主要关注如何找到一组变量的赋值，使得所有约束条件都得到满足。约束可以是逻辑、数值或其他形式的限制，广泛存在于各种实际问题中，如资源配置、日程安排、路径规划等。约束满足问题（CSP）是这类问题的基础模型。 **1. 约束满足问题 (CSP)** CSP 描述了一个问题，其中包含一系列变量、值域和约束条件。每个变量可以取其值域内的某个值，而约束条件则规定了变量之间允许的组合。例如，N 皇后问题要求在棋盘上放置 N 个皇后，使得没有两个皇后在同一行、同一列或同一斜线上。CSP 的关键是找到一种方式来有效地探索所有可能的变量赋值组合，并找出符合所有约束的解。 **2. 约束传播** 约束传播是解决 CSP 的核心算法之一，它通过不断更新和传播约束信息来减少搜索空间。常见的约束传播技术包括 Arc-Consistency（弧一致）和 Domain-Consistency（域一致）。弧一致确保每条边连接的两个变量的值域都只包含能一起满足约束的值；域一致则进一步确保每个变量的值域仅包含能与所有相邻变量兼容的值。这些方法有助于减少无效的搜索，提高求解效率。 **3. 打破对称** 在 CSP 中，可能存在多个解，且这些解在某种意义上是对称的，例如N皇后问题的解可能只是位置上的不同排列。打破对称是指通过特定策略减少对称性，从而减少搜索的重复，加快求解速度。常见的策略包括变量排序、值排序等。 **第二章 SAT 求解算法及相关问题** **1. SAT 相关定义** SAT（Boolean Satisfiability Problem）是确定布尔表达式是否可满足的问题。3-SAT 是一个特殊的 SAT 类型，其中每个子句包含三个变量的布尔运算。SAT 已被证明是NP完全问题，即最复杂的一类计算问题。 **2. 2-SAT 问题和相变** 2-SAT 是一个相对简单的 SAT 特例，因为它可以通过图论的方法快速解决。相变是指随着问题实例的复杂度增加，问题从容易解变为难以解的临界点。在 SAT 中，随着子句密度的增加，问题从几乎总是可满足转变为几乎总是不可满足，这个转变点就是相变点。 **3. SAT 的求解算法概述** 解决 SAT 的算法主要包括回溯搜索、DPLL（Davis-Putnam-Logemann-Loveland）算法及其变体。DPLL 算法结合了单元推理和纯符号消去等启发式策略，是现代 SAT 求解器的基础。 **4. MAX-SAT 问题** MAX-SAT 是 SAT 的一个变种，目标是找到使尽可能多的子句满足的变量赋值，而不是仅仅寻找一个满足所有子句的解。它是优化问题，而非决定性问题。 **5. SMT 问题** Satisfiability Modulo Theories（SMT）是 SAT 的扩展，处理带有背景理论（如整数算术、实数算术、位操作等）的布尔公式。SMT 求解器在软件验证、程序分析和自动定理证明等领域有广泛应用。 **第三章 启发式算法** 启发式算法是一种基于问题特性进行优化的搜索策略，包括局部搜索、模拟退火、遗传算法等。 **1. 局部搜索** 局部搜索算法从问题的一个初始状态开始，通过迭代改变少量变量来逐步改进解的质量，直到达到一个满意的状态。常见的局部搜索算法有 Hill Climbing、Simulated Annealing 和 Genetic Algorithm。 **2. 模拟退火** 模拟退火是一种全局优化方法，借鉴了固体退火过程中能量起伏的概念。它允许在搜索过程中接受较差的解，以避免陷入局部最优。 **3. 遗传算法** 遗传算法受到生物进化过程的启发，通过选择、交叉和变异操作在解的种群中进行迭代，以求得问题的近似最优解。 约束求解和 SAT 求解算法是解决复杂问题的关键工具，涵盖了一系列理论和实践方法，从基础的约束满足到高级的 SMT 解决，以及利用启发式策略来优化搜索过程。这些技术在现实世界中有着广泛的应用，如工程设计、优化调度、自动推理等。