符号模型检验（7）ADD

代数决策图（ADD）是一种用于伪布尔函数表示和操作的图形化数据结构。

Aerozeor

1038人浏览 · 2022-05-08 12:49:20

Aerozeor · 2022-05-08 12:49:20 发布

$⇑⇑⇑⇑⇑\Uparrow\Uparrow\Uparrow\Uparrow\Uparrow$ 上方专栏内有更多内容 $⇑⇑⇑⇑⇑\Uparrow\Uparrow\Uparrow\Uparrow\Uparrow$

ADD

代数决策图（ADD）是一种用于伪布尔函数表示和操作的图形化数据结构。与BDD不同的是BDD只有0,1两个终端节点，但ADD 可以有多个不同终端节点。
n元伪布尔函数：任意一个自变量取值只能是0或1，函数值可为实数的n元函数。
令R表示实数集，B={0,1}，那么n元伪布尔函数可表示为： $B^n\to R$ 。
例如伪布尔函数 $f = x_1x_2 + 2x_3x_4$
伪布尔函数 $f = x_1x_2 + 2x_3x_4$ 在变量序 $π:x1<x2<x3<x4\pi:x_1<x_2<x_3<x_4$ 下的ADD为

再有例子:给出一个自动机，把它转换为ADD形式。

将顶点进行编码0:[00],1:[10],2:[01],3:[11]
$MG=y0y10010011100100111[1201003000030200]x0x1M_G=\begin{matrix} &\begin{matrix}y_0y_1& \quad&\quad&\quad\end{matrix}\\ &\begin{matrix}00&10&01&11\end{matrix}\\ \begin{matrix}00\\10\\01\\11\end{matrix}& \begin{bmatrix}1&2&0&1\\0&0&3&0\\0&0&0&3\\0&2&0&0\end{bmatrix}\\ x_0x_1 \end{matrix}$
转换为ADD为

伪布尔函数可以看作是布尔函数的扩展，即把布尔函数的值域从{0,1}扩展到整个实数域。同样，伪布尔函数也可以按照类似布尔函数的方式进行展开。
定理如果 $f(x1,x2,…,xn)f(x_1, x_2, \dots, x_n)$ 是伪布尔函数，则对于 $∀xi∈x1,x2,…,xn\forall x_i\in{x_1, x_2, \dots, x_n}$ 有：
$(x_1, …,x_{i-1}, x_i, x_{i+1}, …, x_n)= \\x_i \times f (x_1, …,x_{i-1}, 1, x_{i+1}, …, x_n) \\+ (1-x_i) \times f (x_1, …,x_{i-1}, 0, x_{i+1}, …, x_n)$
其中：“ $×\times$ ”、“ $+$ ”和“ $-$ ”分别表示算术运算乘法、加法和减法。

为了便于介绍伪布尔函数的ADD描述，下面用 $x^{'}$ 代表 $(1 - x)$ 。
对于任意伪布尔函数 $f(x1,x2,…,xn)f(x_1, x_2, \dots, x_n)$ ，根据定理有：
$f(x1,x2,…,xn)=x1′f(0,x2,…,xn)+x1f(1,x2,…,xn)=x1′x2′f(0,0,x3,…,xn)+x1′x2f(0,1,x3,…,xn)+x1x2′f(1,0,x3,…,xn)+x1x2f(1,1,x3,…,xn)=x1′x2′…xn′f(0,0,…,0)+x1′x2′…xn−1′xnf(0,0,…,0,1)+⋯+x1x2…xnf(1,1,…,1)f(x_1, x_2, \dots, x_n)= x_1' f (0, x_2, \dots, x_n) + x_1 f (1, x_2,\dots, x_n)\\ = x_1' x_2' f (0, 0, x_3, \dots, x_n) + x_1' x_2 f (0, 1, x_3,\dots, x_n) \\\quad+ x_1 x_2' f (1, 0, x_3, \dots, x_n) + x_1 x_2 f (1, 1, x_3,\dots, x_n)\\ = x_1' x_2' \dots x_n' f (0, 0, \dots, 0) + x_1'x_2' \dots x_{n-1}' x_n f (0, 0,…, 0, 1)\\\quad+ \dots+ x_1 x_2 \dots x_n f (1, 1, \dots , 1)$
其中， $x1′x2′…xn′,…,x1x2…xnx_1'x_2'\dots x_n', \dots , x_1x_2\dots x_n$ 称之为小项，共有2n项； $\dots, 0)，\dots，f (1, 1, \dots, 1)$ 为S中的元素，称之为函数 $f(x1,x2,…,xn)f(x_1, x_2, \dots, x_n)$ 对应小项的系数。

ADD可以看做是对小项的隐式列举，所以ADD可以用小项的系数矩阵来表示。
例如，当n=2时，函数f (x1, x2)的小项系数矩阵为：
$[f(0,0)f(0,1)f(1,0)f(1,1)]\begin{bmatrix}f(0,0)&f(0,1)\\f(1,0)&f(1,1)\end{bmatrix}$

ADD基本操作：
1、布尔操作
2、算术操作
3、提取操作（Abstraction Operation）

1、布尔操作－－ITE (if-then-else)操作
定义　若已知具有相同变量序 $π:x1<x2<⋯<xn\pi:x_1<x_2<\dots<x_n$ 的ADD f，g和h，且f为只具有0和1终结点的ADD，则 $ITE(f,g,h)=f⋅g+f′⋅h{\rm ITE}( f, g, h) = f \cdot g+f'\cdot h$ 。
如果用 $D^f$ , $D^g$ , $D^h$ 和 $D^I$ 分别表示f, g, h和 $ITE(f,g,h){\rm ITE}( f, g, h)$ 的小项系数的集合，则：
$Df={d1f,…,dqf}={f(0,0,…,0),f(0,0,…,1),…,f(1,1,…,1)}D^f=\{d^f_1,\dots,d^f_q\}=\{f(0,0,\dots,0),f(0,0,\dots,1),\dots ,f(1,1,\dots,1)\}$ 　
$Dg={d1g,…,dqg}={g(0,0,…,0),g(0,0,…,1),…,g(1,1,…,1)}D^g=\{d^g_1,\dots,d^g_q\}=\{g(0,0,\dots,0),g(0,0,\dots,1),\dots ,g(1,1,\dots,1)\}$ 　
$Dh={d1h,…,dqh}={h(0,0,…,0),h(0,0,…,1),…,h(1,1,…,1)}D^h=\{d^h_1,\dots,d^h_q\}=\{h(0,0,\dots,0),h(0,0,\dots,1),\dots ,h(1,1,\dots,1)\}$ 　
其中 $(\cdot)\in\{0,1\}$ , $g(⋅)∈Sg(\cdot)\in S$ , $h(⋅)∈S,q=2nh(\cdot)\in S, q=2n$ 。

$DI={ite(d1f,d1g,d1h),ite(d2f,d2g,d2h),…,ite(dqf,dqg,dqh)}D^I=\{{\rm ite}(d^f_1,d^g_1,d^h_1),{\rm ite}(d^f_2,d^g_2,d^h_2),\dots,{\rm ite}(d^f_q,d^g_q,d^h_q)\}$
由定义可知

$difd^f_i$	$digd^g_i$	$dihd^h_i$	$ite(d1f,d1g,d1h){\rm ite}(d^f_1,d^g_1,d^h_1)$
1	-	-	$digd^g_i$
0	-	-	$dihd^h_i$
-	-	$=dig=d^g_i$	$digd^g_i$
-	1	0	$difd^f_i$

例：已知伪布尔函数f、g和h对应的系数矩阵 $M_f$ ， $M_g$ 和 $M_h$ ，分别如下所示，试构造一个用于表示函数 $I = f g + f^{'} h$ 的ADD：
$Mf=[1000110011101111]Mg=[3333333355555555]Mh=[1144114400220022]M_f=\begin{bmatrix}1&0&0&0\\1&1&0&0\\1&1&1&0\\1&1&1&1\end{bmatrix} M_g=\begin{bmatrix}3&3&3&3\\3&3&3&3\\5&5&5&5\\5&5&5&5\end{bmatrix} M_h=\begin{bmatrix}1&1&4&4\\1&1&4&4\\0&0&2&2\\0&0&2&2\end{bmatrix}$
三个矩阵的ADD为

从三个系数矩阵中可以得到I的系数矩阵 $MI=[3144334455525555]M_I=\begin{bmatrix}3&1&4&4\\3&3&4&4\\5&5&5&2\\5&5&5&5\end{bmatrix}$

2、算术操作
定义　若已知表示具有相同变量序 $π:x1<x2<⋯<xn\pi:x_1<x_2<\dots<x_n$ 的伪布尔函数 $ϕ\phi$ 和 $φ\varphi$ 的ADD f和g，及二元运算符op，则 $Apply(f,g,op)=f⟨op⟩g{\rm Apply} (f, g, op) = f \langle op \rangle g$ .
op： $+$ 、 $-$ 、 $×\times$ 、 $÷\div$ 、min和max等算术操作。
$Apply(f,g,op){\rm Apply} ( f, g, op)$ 操作的本质：设 $D^f$ 、 $D^g$ 和 $D^A$ 分别表示f、g和 $Apply(f,g,op){\rm Apply} ( f, g, op)$ 的小项系数的集合，则：
$Df={d1f,…,dqf}={f(0,0,…,0),f(0,0,…,1),…,f(1,1,…,1)}D^f=\{d^f_1,\dots,d^f_q\}=\{f(0,0,\dots,0),f(0,0,\dots,1),\dots ,f(1,1,\dots,1)\}$ 　
$Dg={d1g,…,dqg}={g(0,0,…,0),g(0,0,…,1),…,g(1,1,…,1)}D^g=\{d^g_1,\dots,d^g_q\}=\{g(0,0,\dots,0),g(0,0,\dots,1),\dots ,g(1,1,\dots,1)\}$

$DA={d1f⟨op⟩d1g,…,dqf⟨op⟩dqg}D^A=\{d^f_1\langle op \rangle d^g_1,\dots,d^f_q\langle op \rangle d^g_q\}$

例：已知伪布尔函数f和g对应的系数矩阵 $M_f$ 和 $M_g$ ，分别如下所示，试构造一个用于表示函数 $A = f + g$ 的ADD
$Mf=[0011001111001100]Mg=[3333333322222222]M_f=\begin{bmatrix}0&0&1&1\\0&0&1&1\\1&1&0&0\\1&1&0&0\end{bmatrix} M_g=\begin{bmatrix}3&3&3&3\\3&3&3&3\\2&2&2&2\\2&2&2&2\end{bmatrix}$
可以得到A的系数矩阵 $MA=[3344334433223322]M_A=\begin{bmatrix}3&3&4&4\\3&3&4&4\\3&3&2&2\\3&3&2&2\end{bmatrix}$
设行以 $x_0'x_1',x_0x_1',x_0'x_1,x_0x_1]$ 标记，列以 $y_0'y_1',y_0y_1',y_0'y_1,y_0y_1]$ 标记，则f,g,A的ADD：

3、提取操作（Abstraction Operation）
通过对函数变量的提取可减少函数维数。例如，当函数表示的是一个 $N×N(N=2p)N\times N(N=2p)$ 的矩阵时，设矩阵行和列分别由布尔变量 $x0,x1,…,xpx_0,x_1,\dots,x_p$ 和 $y0,y1,…,ypy_0,y_1,\dots,y_p$ 表示，则通过对矩阵提取行变量 $x0,x1,…,xpx_0,x_1,\dots,x_p$ ，便可得到行向量，即 $1×N1\times N$ 的矩阵，从而减少原矩阵的维数
$fxop(y)=∖xopf(u)=op1⃗x=0⃗f(u),u=xy‾∈{x0x1…xpy0y1…yp}f^{op}_ \bm x(\bm y)=\setminus^{op}_\bm xf(u)=\underset{\bm x=\vec 0}{\overset{\vec 1}{op}}f(u),u=\overline{\bm x\bm y}\in\{x_0x_1\dots x_py_0y_1\dots y_p\}$
例如，假设函数 $f = A (X, Y)$ 表示某个 $n×mn\times m$ 矩阵 $M$ ，其中
$X={x0,x1,…,xp}(p=log2n)X=\{x_0,x_1,\dots,x_p\}(p=log_2n)$ 是行变量编码，
$=\{y_0,y_1,\dots,y_q\}(q=log_2m)$ 是列变量编码。
$∖X+A(X,Y)\setminus^+_XA(X,Y)$ ：对同一列元素求和，其结果是一个 $1×m1\times m$ 矩阵

$∖X×A(X,Y)\setminus^\times_XA(X,Y)$ ：对同一列元素求积，其结果是一个 $1×m1\times m$ 矩阵
$∖YminA(X,Y)\setminus^{min}_Y A(X,Y)$ ：求每一行元素的最小值，其结果是一个 $n×1n\times 1$ 矩阵

例：给出矩阵 $f = A (X, Y)$ ，计算 $∖X+A(X,Y)\setminus^+_XA(X,Y)$ ， $∖YminA(X,Y)\setminus^{min}_Y A(X,Y)$
$A=[1234567800122222]A=\begin{bmatrix}1&2&3&4\\5&6&7&8\\0&0&1&2\\2&2&2&2\end{bmatrix}$
计算有
$∖X+A(X,Y)=[8101316]∖YminA(X,Y)=[1502]\setminus^+_XA(X,Y)=\begin{bmatrix}8&10&13&16\end{bmatrix}\quad\setminus^{min}_Y A(X,Y)=\begin{bmatrix}1\\5\\0\\2\end{bmatrix}$

例2：给出矩阵 $f = A (X, Y)$ ，设行以 $x_0'x_1',x_0x_1',x_0'x_1,x_0x_1]$ 标记，列以 $y_0'y_1',y_0y_1',y_0'y_1,y_0y_1]$ 标记。
$A=[1502260237124822]A=\begin{bmatrix}1&5&0&2\\2&6&0&2\\3&7&1&2\\4&8&2&2\end{bmatrix}$
则
$∖{x0,y0}+A(X,Y)=∖{y0}+B(X,Y)=[144227]\setminus^+_{\{x_0,y_0\}}A(X,Y)=\setminus^+_{\{y_0\}}B(X,Y)=\begin{bmatrix}14&4\\22&7\end{bmatrix}$
$∖{x0,x1,y0}minA(X,Y)=∖{y0}minC(X,Y)=[10]\setminus^{min}_{\{x_0,x_1,y_0\}}A(X,Y)=\setminus^{min}_{\{y_0\}}C(X,Y)=\begin{bmatrix}1&0\end{bmatrix}$
其中 $B(X,Y)=[3110471534]B(X,Y)=\begin{bmatrix}3&11&0&4\\7&15&3&4\end{bmatrix}$ ， $C(X,Y)=[1502]C(X,Y)=\begin{bmatrix}1&5&0&2\end{bmatrix}$

这里如果细心的话可以注意到之前所有设计出的行标记和列标记是故意没有按照枚举顺序。

例3：已知ADD，求 $∖{x0,y0}+A(X,Y)\setminus^+_{\{x_0,y_0\}}A(X,Y)$

我们令 $r_u$ 代表提取操作中步骤的子图。例如
$r=∖{x0,y0}+f(u)r_{}=\setminus^+_{\{x_0,y_0\}}f(u)$
$r1=∖{y0}+f(u)∣x0=1r_{1}=\setminus^+_{\{y_0\}}f(u)|_{x_0=1}$
$r10=∖{y0}+f(u)∣x0=1,x1=0r_{10}=\setminus^+_{\{y_0\}}f(u)|_{x_0=1,x_1=0}$
$r101=∖{}+f(u)∣x0=1,x1=0,y0=1r_{101}=\setminus^+_{\{\}}f(u)|_{x_0=1,x_1=0,y_0=1}$
在达到形式 $r_{abc}$ 下可以发现提取操作下没有元素需要提取。
所以
$rabc=∖{}+f(u)∣x0=a,x1=b,y0=c=f(u)∣x0=a,x1=b,y0=cr_{abc}=\setminus^+_{\{\}}f(u)|_{x_0=a,x_1=b,y_0=c}=f(u)|_{x_0=a,x_1=b,y_0=c}$
即本题下形如 $r_{abc}$ 的提取操作的子图就是ADD的子图。
我们又知
$rab=∖{y0}+f(u)∣x0=a,x1=b=Σy^0f(u)∣x0=a,x1=b,y0=y^0=f(u)∣x0=a,x1=b,y0=0+f(u)∣x0=a,x1=b,y0=1=rab0+rab1r_{ab}=\setminus^+_{\{y_0\}}f(u)|_{x_0=a,x_1=b}\\ =\underset{\hat y_0}\Sigma f(u)|_{x_0=a,x_1=b,y0=\hat y_0}\\ =f(u)|_{x_0=a,x_1=b,y0=0}+f(u)|_{x_0=a,x_1=b,y0=1}\\ =r_{ab0}+r_{ab1}$
即 $rab=Apply(rab0,rab1,+)r_{ab}={\rm Apply}(r_{ab0},r_{ab1},+)$
对于 $r_a$
$ra=∖{y0}+f(u)∣x0=a=x1∖{y0}+f(u)∣x0=a,x1=1+x1′∖{y0}+f(u)∣x0=a,x1=0=x1ra1+x1′ra0=ITE(x1,ra1,ra0)r_a=\setminus^+_{\{y_0\}}f(u)|_{x_0=a}\\ =x_1\setminus^+_{\{y_0\}}f(u)|_{x_0=a,x_1=1}+x_1'\setminus^+_{\{y_0\}}f(u)|_{x_0=a,x_1=0}\\ =x_1r_{a1}+x_1'r_{a0}\\ ={\rm ITE}(x_1,r_{a1},r_{a0})$

同理可得 $r=Apply(r0,r1,+)r={\rm Apply}(r_{0},r_{1},+)$
可以看到这整个过程就是二叉结构自底向上构建。这也是提取操作的计算步骤。
需要提取的元素就是用apply运算，不需要的则是ite运算

天启AI社区

GitCode 天启AI是一款由 GitCode 团队打造的智能助手，基于先进的LLM（大语言模型）与多智能体 Agent 技术构建，致力于为用户提供高效、智能、多模态的创作与开发支持。它不仅支持自然语言对话，还具备处理文件、生成 PPT、撰写分析报告、开发 Web 应用等多项能力，真正做到“一句话，让 Al帮你完成复杂任务”。

更多推荐