计算机中使用的数理逻辑学习笔记

布尔代数运算律

布尔运算等式变换

\[\begin{matrix} \overline{x_1 \cdot x_2} = \overline{x_1} + \overline{x_2} \\ (x \vee z)(x \vee y) = xx \vee xz \vee xy \vee zy = x \vee zy \end{matrix} \]

BDD(二元决策树)

BDD描述了一个过程，这个过程按照给定的值（0/1）进行向下搜索，直到终点。

![](https://img2018.cnblogs.com/blog/1503464/201912/1503464-20191231105949829-2067411705.png)

从真值表中派生（Derive）二元决策树：

化简：将冗余的部分去掉

对于左边红框内，因为无论$C$取何值，最终的结果总是为0，因此$C$的存在对于该分支的结果并没有影响，因此可以将其删除。对于右边红框由$B$延伸到$C$处时，无论$B$取何值，总是延伸到相同的$C$，因此在这里$B$的取值也对该分支没有影响，因此可以直接将$B$节点删除，从而得到了右图。

Shannon expansion formula(香农展开)

\[f(A, B, C,...) = Af(1,B,C) \vee \overline{A}f(0,B,C,...) \]

算法步骤：

固定一个变量，画出此变量的节点以及01分支
看是否有分支可以合并，如果可以则合并，否则再选取另一个变量转到步骤1
直到分支节点处变为0或1，则结束。

即：每次提取一个变量，将原来的表达式扩展为该变量取不同值的形式。
示例：

如图a所示，将$A$取值为0时，原表达式$f$进化为为$f_0$，将$A$取值为1时，$f$进化为$f_1$。

BDD在计算机中的存储时，每个节点对应一个三元组：(变量名称，指针1，指针2)
其中，变量名称指定变量，指针1，指针2分别指定，当前变量取值分别为0或1时，应该指向的节点。

如(a)表示一个节点分支，则其在计算机中的存储可以表示为(V, g, h)。(b)表示了一组存储的三元组。(c)表示了(b)代表的BDD。

计算BDD的输出时，只需要沿着标识路径一直往下走即可，所到达的终止节点的值即为输出结果。

注：

一个节点的输出路径有且仅有一条是active path
从一个节点到0或1终点，有且仅有一条由active path组成的路径

计算“和的积”与“积的和”的个数
“和的积”的个数：主合取范式中，合取式的个数，即：使输出结果为0的路径数目。
“积的和”的个数：主析取范式中，析取式的个数，即：使输出结果为1的路径数目。

用分支的权值计算：
步骤：

最上层结点的两个分支权均赋值为1。
其余的结点的两个分支权均赋值为它所有入度权值的和。

其中，和的积(0): 8+7+7=22 积的和(1): (8+8+7=23)

图的简化(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)反过来做即可。

举例：$f=(x_1+x_2)*x_3+x_4,g=x_1*x_3^{\'}+x_4$，求$f+g$的OBDD

关于 OBDD 的 ITE 的实现过程
ITE操作是一个三元布尔操作符，对于具有相同变量序的三个布尔函数f、g和h，ITE操作可用来实现：if f then g else h。对于相同变量序：$x_1<x_2<...<x_n$下的布尔函数$f,g$和$h$,$ITE(f,g,h)=f\cdot g+f^{\'}\cdot h$
在算法中，常用小写 ite 来表示 ITE。下表给出了一些二元布尔运算的 ITE 操作实现:

程序转化为逻辑表达式

FDS(Fair Discrete System)

一个Fair Discrete System(FDS) $D = \lt V, O, \Theta, p, J, C \gt$包括：

$V$：一组有限的类型化状态变量，一个V-state s表示V的一个解释
$ \sum_V $：表示所有的V-states集合
$O \subseteq V$: 可观察变量的集合
$\Theta $：一个初始条件。一个描述初始状态的能够满足的断言
$p$：一个过渡关系。一个断言$p(V, V^{\'})$，引用状态变量的当前版本和即将变换成的版本。例如，$x^{\'}=x+1$对应于赋值$x:=x+1$
$J={J_1,...,J_k}$：一个公平的(justice)需求集合。确保对于每个$j_i,i=1,...,k$的计算包含无限多个$j_i$-states。
$C=\lbrace <p_1,q_1>,...,<p_n,q_n>\rbrace$：一个包含compassion需求的集合。无限多个$p_i$-states意味着无限多个$q_i$-states。

例子：

首先表示$V$，状态变量

\[V:\left( \begin{matrix} x,y: natural \\ \pi_1: \lbrace l_0,l_1,l_2\rbrace \\ \pi_2: \lbrace m_0,m_1 \rbrace \end{matrix} \right) \]

a) 首先第一行就是程序最上面的初始化，左边两个变量一写，右边写个 natural。
b) 接下来定义$\pi $，程序有几个部分(用||连接)就定义几个$\pi $，每个$\pi $对应的元素就是每一行语句$

秒客网