数理逻辑笔记整理
作者：互联网
布尔代数
析取：∨，逻辑或
合取：∧，逻辑与，通常省略或使用’·‘（点乘）代替
可以列出的最小元素0，最大元素1和任何元素a及其补a‘都是唯一确定的。
OBDD（有序二元决策树）
将逻辑语言使用二叉决策图的形式表示
真值表与BDD
化简：去除冗余部分
香农展开·决策图算法步骤
对于布尔函数的展开：
- 固定一个变量，画出此变量的节点以及0，1分支
- 观察是否有冗余分支存在，存在则合并；否则再选取另一个变量，转至步骤1
- 直至分支节点处变为0或1，结束
总结：逐层确定变量取值，对应改变布尔表达式。
BDD再计算机存储中，每个节点对应一个三元组：<变量名，指针1，指针2>
其中，指针1，2分别指向当前变量取值为0和1时的节点。
计算BDD输出·算法步骤
- 在图中标识所有被赋值（取决于布尔表达式）的路径，这些路径称为active path
- 沿着active path取至终点。
注：
- 一个节点的输出路径有且仅有一条是active path
- 从一个节点到0或1终点，有且仅有一条由active path组成的路径
计算“和的积”与“积的和”的个数
“和的积”的个数：主合取范式中，合取式的个数，即：使输出结果为0的路径数目。
“积的和”的个数：主析取范式中，析取式的个数，即：使输出结果为1的路径数目。
用分支的权值计算：
步骤：
- 最上层结点的两个分支权均赋值为1。
- 其余的结点的两个分支权均赋值为它所有入度权值的和。
图的简化(reduce) (ODBB)
简化后的函数图包含以下性质：
- 不包含左右子节点相同的节点
- 不包含这样的节点：分别以左右子节点为根节点的子图同形
注：在简化的图中，以每一节点为根的子图也是简化的。任意的布尔函数有唯一的简化图可以将其表示，使得图的节点数目最少
化简思想为：将原图按层排列，从终止节点(底层)依次向上进行标记，最后相同标记的只取一个节点就完成了图的简化。
步骤：
- 将节点放到各层列表中，此处要注意的是，要把终止节点全部放在最后一层
- 从终止节点到根节点对每层的list进行操作：
- 对于每个节点，oldkey的初始化均为(-1,-1)，终止节点的oldkey最后应该只有一个0或1值，同时终止节点最终也应该至多只有两个id(1,2)和oldkey(0,1)
- 对于非终止节点，其oldkey最后为两个值，前一个值表示其取0时应该指向的节点id，另一个值表示其取1时应该指向的节点id。low,high分别表示其取0和1时指向的节点。
- 当某个节点的low值和high值相等时，说明该节点的取值对于该分支的最终结果并没有影响，因此可以直接删除该节点。
OBDD的Apply操作
通过深度优先搜索的方法，对一些已知的布尔函数 OBDD 表示进行二元布尔运算得到另外一些布尔函数 OBDD 表示的操作。整个过程从上至下进行，我们需要做的预备工作是给每个节点编号（1，2，3.... 每个都不相同），然后从顶层开始，用两个 OBDD 树的顶层的节点合成一个新的节点，合成的规则就三种：
- 两个节点都为叶节点，可以直接根据布尔运算得出结果，合成的节点也是叶节点。
- 如果有一个节点为非叶子节点，看这两个节点的 index 值是否一样，如果是一样的，比如两个节点都表示 x1，那么新节 点的 index 就是 x1，新节点的左孩子通过两个老节点的左孩子生成，新节点的右节点通过两个老节点的右孩子生成。
- 如果两个节点的 index 值不同，比如 index(u)<index(v)，新节点的 index 为较小的 index(u)，新节点的左孩子由 u 的左孩子与 v 生成，新节点的右孩子由 u 的右孩子与 v 生成，当 index(u)>index(v)反过来做即可。
举例：
标签：index,分支,笔记,active,整理,OBDD,节点,数理逻辑,布尔 来源： https://www.cnblogs.com/lyle0411/p/14168111.html