约束求解公开课笔记
两种计算思维
- 符号主义（约束求解）：问题可以清晰描述 Typical：定理证明
- 连接主义（机器学习）：问题难以清晰描述 Typical：模式识别
约束求解
- 建模：用数学语言对问题进行形式化表达
约束模型分为：
- SAT问题，电路SAT，Max SAT
- (非)线性规划，二次规划，0-1规划，整数（非）线性规划，混合整数（非）线性规划
- 一阶逻辑可满足性问题，QBF，SMT，MaxSMT，OMT
SAT问题
- 布尔可满足性问题，命题逻辑可满足性问题
- 给定一个命题逻辑公式，判断是否存在使其为真的赋值
- 合取范式（CNF）:用and连接每个字句
如何识别问题的约束：包含三个方面，1）事实、规则 2）必须做的 3）不能违反的
- SMT:限定背景理论的一阶逻辑
- 好的约束模型：形式化，一般性，可求解
- Tseitin编码： 任意命题逻辑公式转为CNF公式
SAT应用
- 电路等价性验证
- 有界模型检测（Bounded Model Checking）：检查在K步之内，是否存在一条路径，违反了指定的属性（时序逻辑公式）
- 密码分析
SMT = SAT + 很多理论
应用：硬件验证，字级别验证，软件验证，线性规划
规划方式
- 整数线性规划：资源分配问题
- 混合整数规划：生产规划，供应链优化
CSP模型
- Constraint Satisfaction Problem 约束可满足问题
- 一个CSP被看作是一个三元组<V,D,C>，其中V是变量的集合，D是每个变量的值域，C是一组约束。
- 问题的目标是求一个对变量的赋值，该赋值满足C中所有的约束
- 一个特点：全局约束
- 采取哪个约束模型，主要考虑：表达的便易性，求解器的性能，有时候需要配合不同模型求解器
求解器：求解一个约束模型的程序
- 约束求解的两类方法：
- 完备算法/精确算法：算法结束时确保问题最优解，往往难以解决大规模问题
- 不完备算法/启发式方法：不保证最优解，争取在短时间返回解（近似解）
分支启发式
- Fail Fast原则
SAT： Variable State Independent Decaying Sum 每个变量维护一个活跃分数，挑选最大分数的变量 初始化为其出现次数 每次产生一个新的冲突子句：该子句的所有变量增加分数 周期性的对所有分数都乘以一个小于1的正常数
CSP分支启发式： dom 启发域的大小 / wdeg加权的度 每个变量维护一个分数 dom/wdeg ，dom为变量的实时可行域大小，wdeg（加权度）衡量了变量参与冲突的次数，挑选最小分数的变量 Wdeg初始化为变量出现的约束个数，也就是变量的度数 每次遇到一个新的冲突约束：该约束的所有变量的wdeg增加1 周期性的遗忘wdeg
分支策略：
- 多分支：x = a, b, c , …
- 二分支（常用）：x 等于或者不等于 a
分支限界方法（主流）
- strong branch：对每个变量v，计算分支它得到的两个子问题的下界（通过LP松弛）。选择产生的下界的最佳的变量进行分支
- Pseudo Cost Branch：选择历史上单位变化对LP松弛目标函数的增大量最大的变量进行分支。需要前序分支策略来作为历史信息参考（一般为Strong Branch）
- 综合策略：实际常用的多为综合策略，如reliability branch
约束传播
- SAT：布尔约束传播（单元传播）
- CSP: 弧一致性。 每个变量的值域中的所有值都满足它的所有二元约束。
域传播
- 通过分析约束和当前变量域，进一步缩小变量域
不完备算法：局部搜素
- 从一个完整赋值开始。迭代的选择变量进行翻转。在搜索空间，从一个点出发，跳到邻居点
- 需要定义领域关系，一般通过算子定义
- 局部最优是相对于一个解空间来说的
CNF
合取范式Conjunctive Normal Form
### SAT Input File DIMACS format
c example //注释行
p cnf 变量数 字句数 //定义一个cnf