代课老师：刘西洋
课件下载：https://github.com/mathematical-logic/mathematical-logic
参考："好心人"的往年总结
从莱布尼兹之梦到冯-诺依曼计算机
命题逻辑的有序二叉决策图（OBDD）
题型 1:根据真值表画出 BDD，或根据公式画出 BDD。
三步走(不断利用香农展开的过程):
a) 固定一个变量，画出此变量的节点及 0 1 分支。
b) 看是否有分支可以合并，如果可以则合并，否则再选取另一个变量转到步骤 a)。
c) 直到分支节点处变为 0 或 1，则结束。
题型 2:化简图
这里就使用 PPT 里面给的那个 Reduction 操作。这里把流程 走一遍。
题型 3:给出两个 f，对其进行<op>操作。
这题需要两步， 第一步是 Apply 操作，将两个图合并成一个图，第二步是 Reduction 操作，就 是上面的化简。
a) f1 的根结点 v1，f2 的跟结点 v2，操作为<op>，
整个过程就是在 f1 中取一个结点，在 f2 中取一个结点，然后比较
b) 如果 v1 和 v2 均为终止结点，那么目标图上画一个终止结点，值为 v1<op>v2
c) 如果 v1 和 v2 都不是终止结点，那就比较他们的索引值。
1. 如果 index(v1) = index(v2) = i，目标图画一个非终止结点，对应 index = i;
然后在 low(v1)和 low(v2)递归地应用该算法，深度优先，完成之后，在 high(v1)和 high(v2)递归地应用该算法。
2. 如果 index(v1) = i，index(v2) > i，目标图画一个非终止结点，对应 index = i;然后，在子树中递归调用该算法。
d) 如果 v1 和 v2 一个是非终止结点，另一个是终止结点，终止结点的值是x
1. 如果 x<op>v2 的值由 x 决定，目标图上画一个终止结点，值为 x。
2. 如果 x<op>v2 的值不由 x 决定，目标图上画一个非终止结点，index = index(v2)
命题逻辑基于SAT Solver的DPLL可满足性判定算法
DPLL Framework
DPLL（Davis-Putnam-Logemann-Loveland）算法，是一种完备的、以回溯为基础的算法，用于解决在合取范式（CNF）中命题逻辑的布尔可满足性问题；也就是解决CNF-SAT问题。DPLL是一种高效的程序，并且经过40多年还是最有效的SAT解法，以及很多一阶逻辑的自动定理证明的基础。
Some conception:
1. 文字:一个变量或者它的补。
2. 子句:合取范式中两个合取符号间的部分叫子句。
3. 单元子句、单元文字:子句中其他变量的逻辑值都为 0，只剩一个文字未被赋值，
则该文字是单元文字，对应的子句是单元子句。
4. 矛盾子句:子句中所有文字的逻辑值都为 0。
5. 可满足问题:一个合取范式，存在一组赋值使所有子句的逻辑值都为 1。
6. SAT 求解算法:1. 局部搜索算法(不完备算法);2. DPLL 算法(完备算法)
1、如果文字a（正文字或者负文字）在子句c（clause）中出现并且在其它子句中未出现!a，那么删除该子句。
`删除后所得公式与原公式具有相同的可满足性！`
2、`任意选择`一个文字b，并且对b赋值“真” (V = {b}) ，删除包含b的子句，并且把所有其余子句中的!b删除。
3、对`只剩余一个文字的子句赋值`，使该文字为真（扩大the partial valuation V＝ {b，!C} ）。
4、如果the partial valuation有矛盾赋值（contradictory valuation），例如 V = {b, !C, C} ，
`退回原来的选择`（backtrack to the privous choice），重新对文字b赋值 V= {!b} .
5、如果已经没有办法回退，则该公式不可满足（unsatisfiable）
- Recursive description
DPLL(formula, assignment){
necessary = deduction(formula, assignment); # 找出必要的变量赋值
new_asgnmnt = union(necessary, assignment); # 得到新的一组赋值
if (is_satisfied(formula, new_asgnmnt)) # 判断是否可满足
return SATISFIABLE;
else if (is_conflicting(formula, new_asgnmnt)) # 判断是否出现冲突
return CONFLICT;
var = choose_free_variable(formula, new_asgnmnt); # 挑选一个未赋值变量
asgn1 = union(new_asgnmnt, assign(var, 1)); # 给未赋值变量赋 1，得到新的赋值
if (DPLL(formula, asgn1)==SATISFIABLE) # 递归判断
return SATISFIABLE;
else {
asgn2 = union (new_asgnmnt, assign(var, 0)); # 给未赋值变量赋 0
return DPLL(formula, asgn2); # 递归判断
}
}
- Iterative Description
status = preprocess(); # 预处理
if (status!=UNKNOWN) return status;
while(true) {
decide_next_branch(); # 变量决策
while (true) {
status = deduce(); # 推理(BCP)
if (status == CONFLICT) {
blevel = analyze_conflict(); # 冲突分析
if (blevel == 0) # 如果冲突层次为顶层，则逻辑式直接不可满足
return UNSATISFIABLE;
else backtrack(blevel); # 智能回溯
}
else if (status == SATISFIABLE)
return SATISFIABLE;
else break;
}
}
迭代比递归的优势:
- 递归速度慢且容易发生溢出，相对于迭代就有很多自身的劣势。
- 迭代具有非时间顺序回溯(智能回溯)的优势。
预处理:所谓预处理就是根据逻辑蕴含推理以及冗余子句删除和添加等值子句等相关技术。
变量决策:如何快速有效地决策出下一个将要赋值的变量。
MOM 方法:
思想:如果一个子句长度很小，那它就很不容易被满足，所以我们要优先考虑它们，给予它们更高的权重。
方法要点:子句长度短，出现频率高。-
VSIDS 方法:
- 为每一个变量设定一个 score，这个 score 的初始值就是该变量在所有子句集中出现的次数。
- 每当一个包含该文字的冲突子句被添加进子句库，该文字的 score 就会加 1。
- 哪个变量的 socre 值最大，就从这个变量开始赋值。
- 为了防止一些变量长时间得不到赋值，经过一定时间的决策后，每一个变量的 score 值都会被 decay，具体方式是把 score 值除以一个常
数(通常为 2-4 左右)。——“周期衰减”
优点:统计数据与变量赋值状态无关，因此系统资源开销非常低。可以 显著提高求解器性能。
BCP：通过推理来减少一些不必要的搜索，加快效率。主要依赖单元子句规则
Counters 方法:每个子句有两个计数器，一个记录逻辑值为 true 的文 字数，另一个记录逻辑值为 false 的文字数。如果一个 CNF 实例有 m 个子句，n 个变量，每个子句平均有 L 个文字，则有一个变量被赋值 的时候，会有平均 mL/n 个计数器需要更新，在回溯的时候，每取消 一个变量赋值，也会平均有 mL/n 个计数器的更新。如果一个子句的false 计数器的值等于该子句的文字数，则说明出现了冲突;如果一 个子句的 false 计数器的值等于该子句的文字数减 1，则该子句是单元子句。
head/tail 方法:每个子句存在一个数组中，并且有两个指针，一个头指针，一个尾指针，每个变量 v 有四个附加链表，分别装有句头是 v 的子句，句头是非 v 的子句，句尾是 v 的子句，句尾是非 v 的子句。 所以，如果有 m 个子句，四个链表中就存放着 2m 个子句。移动指针有四种情况:
1. 第一个遇到的文字为真，说明子句已经满足，直接忽略该子句。
2. 第一个遇到的文字未赋值且不是句尾，那就将该子句删除，放到对应文字的链表中。
3. 头尾指针之间只有一个变量未赋值且其他文字都为假，则出现单元子句。
4. 头尾指针之间所有文字都为假，产生冲突，回溯。
当一个变量被赋值的时候，平均有 m/n 个子句需要更新(m 为子句 数，n 为变量数)。
- 2-literal watching 方法(应用于 zChaff 求解器):与 head/tail 方法相 似，为每个子句关联两个指针，但这两个指针没有头和尾之分，位置 任意。它与 head/tail 方法的关键区别是回溯时指针的位置无需移动， 取消一个变量的赋值时间的开销是常量，但坏处是只有遍历完所有 文字才能找到单元文字。两个指针随时监视子句中任意两个未被赋 值为 0 的文字。每个变量 v 有两个附加链表，对应变量的正负形态， 存放的是对应的子句。设初始时变量 v 赋值为 1，则搜索将在一个含 有文字-v 的子句中进行(因为 v 已满足)，并且此时一个监视指针指 向文字-v，继续搜索，该过程中有四种情况:
1. 如果存在文字 L 不是该子句的另外一个被监视文字，则删除指向文字-v 的指针，
并添加指向文字 L 的指针，相当于指针移动。
2. 如果唯一符合条件的文字 L 是另外一个被监视文字，且它没有被赋值，
则该被监视文字是单元文字，该子句是单元子句。
3. 如果唯一符合条件的文字 L 是另外一个被监视文字，且它已经被赋值为 1，
说明该子句已经满足，不需要进行任何处理。
4. 如果所有文字都已经被赋值为 0，那么出现冲突，回溯。
冲突分析
- Conflict Analysis and Learning 寻找冲突的原因并学习
analyze_conflict(){
cl = find_conflicting_clause();
while (!stop_criterion_met(cl)) {
lit = choose_literal(cl);
var = variable_of_literal( lit );
ante = antecedent( var );
cl = resolve(cl, ante, var);
}
add_clause_to_database(cl);
back_dl = clause_asserting_level(cl);
return back_dl;
}
智能回溯
- 时序回溯:直接返回上一层，将变量取值翻转。
- 非时序回溯:结合冲突学习，智能分析，跳回多个决策层，并且会将导
致冲突的子句加入到子句集中。
子句数据结构
- 数组方式:数组采用连续空间存储，内存利用率和存储效率更高，局部访问能力更强。连续存储能提高 cache 命中率，从而增加计算速度。但不灵活。
- 链表方式:便于对子句进行增加和删除操作，存储效率低。因为缺少局部访问能力，往往会造成缓存丢失。
注:head/tail 和 2-literal watching 都被称为“膨胀数据结构”，它们都采用数组存储子句，最具竞争力。
例题:设计一个基于数组的数据结构存储子句
方案 1:head/tail
用数组存储子句的文字，对于每个数组设置两个指针，分别为头指针 与尾指针，然后对于每个变量 v 设置 4 个链表，分别装有句头是 v 的子句， 句头是非 v 的子句，句尾是 v 的子句，句尾是非 v 的子句，这样存储的子 句，无论子句顺序及其中变量顺序的改变都不会影响所有变量的四个链表中 的子句数量。取所有变量 v 是句头的子句与非 v 是句头的子句或者 v 是句尾 的子句与非 v 是句尾的子句合取可以得到公式。
方案 2:2-literal watching
为每个子句关联两个指针，这两个指针位置任意，随时监视子句中任
意两个未被赋值为 0 的文字。每个变量 v 有两个附加链表，对应变量的正负 形态，存放的是含有对应文字的子句。该种结构的好处是回溯时指针的位置 无需移动，取消一个变量的赋值时间的开销是常量。此外，重新分配最近分 配和未分配的变量将比第一次分配的变量更快，并且可以减少内存访问总数， 提高缓存命中率。
FDS
一个程序 D 由五部分组成𝐷 = < 𝑉,𝑂,𝜃,𝜌,𝐽,𝐶 >
𝑉:有限状态集合。包括程序中的变量和语句.
𝑂:可观测状态集合。定义𝑂属于𝑉。一般没有说明的话，默认所有状态都可观测，因此𝑂等于𝑉。这个不重要，应该不考.
𝜃:初始条件.
𝜌:转换关系。考察的重点.
𝐽:justice 集合，弱公平的.
𝐶:compassion 集合，强公平的.
Alloy
