转载请务必注明出处：https://www.cnblogs.com/the-wind/p/15764283.html

1 背景介绍：两级逻辑

　　香农在他的硕士论文[1]中提出了开关电路的综合方法，其中提到香农展开定理，即任意n变量布尔函数(f(x_1,…,x_{n-1},x_n))都可展开为SOP：

　　亦可根据布尔代数的对偶性得到等价的POS形式。SOP或POS对应布尔网络深度为2，现在一般称为两级逻辑。

　　这种方法很容易综合组合逻辑，其缺点是对于特定布尔函数存在指数爆炸问题（结点数可达(O(n^2))），此外各结点的扇入扇出一般较高。为了降低开销，需要进行逻辑化简。

　　两级逻辑化简是输出限制于SOP/POS形式的逻辑化简。之所以希望输出仍然是两级逻辑，是因为两级逻辑具有特定优势，例如物理结构规则，传播延迟低等，过去常见于可编程逻辑器件（PLD）中。

2 Quine-McCluskey两级逻辑化简

　　一些概念：

变元：x1,x2,…xn
文字：变元或其否定：x1, x1′,…
子句（乘积项）：文字的合取：x1x2, x1’x2,…

　　逻辑化简本质上是对表达式进行等价转化以最小化代价函数的优化过程，其中代价函数评估了表达式的优劣（如对应电路的PPA）。定义SOP表达式E的代价函数为：

　　给定布尔函数f，(argminlimits_{E=f} mathcal{L}(E))即为两级逻辑化简的结果，其中E必须是SOP表达式。

　　(argminlimits_{E=f} mathcal{L}(E))具有最小的电路面积，这是因为E的子句的个数决定第二级逻辑(OR)的面积，文字的个数决定第一级逻辑(AND)的面积。

　　根据卡诺图，容易想到如下算法：对f的所有最小项，利用并项法则（xy + x’y = y）合并相邻两项（恰有一对互补的变元，其余文字相同），其结果是代价函数减少了2（子句个数和文字个数都减少1）。对合并得到的所有子句迭代地应用并项法，直到无法合并为止，所得子句的析取显然与f是逻辑等价的，且代价函数小于等于初值。

　　不幸的是，这方法有时不能得到最优解，举反例证明：f=xy’+x’y+yz’+y’z，无法对其应用并项法，算法结束，但事实上f=xy’+x’y+yz’和f=xy’+x’y+y’z都比原式更简。这种启发式失败了。幸运的是Quine通过引入素蕴涵项成功解决了问题，而素蕴涵的求解与上述过程类似。

　　要理解素蕴涵的概念，需要一些前置知识，准备好后我们将结合Quine[2]的定理，证明：

定理1：代价函数(mathcal{L}(E))定义的最小SOP表达式一定是素蕴涵项之析取

　　这定理提供了Q-M算法的核心思路：在E的素蕴涵项的组合中寻找答案。

2.1 蕴涵项与素蕴涵项

　　首先需要明确ON/OFF集与无关DC集（Don’t care set）的概念。逻辑函数(f: {0,1}^n rightarrow {0,1,*})，f的反函数记为(f^{-1})。ON定义为(f^{-1}(1))，即f=1的所有最小项。OFF定义为(f^{-1}(0))。DC定义为(f^{-1}(*))。一个逻辑函数f可以表示为(f=ON cup DC)。

　　例如，给定逻辑函数g(x,y,z)=xy+z，无关项xyz，其ON集为{xyz’,x’y’z,x’yz,xy’z}，DC集为{xyz}，OFF集为{x’y’z’,x’yz’,xy’z’}。

　　给定函数f和从句p，如果(p subseteq ON cup DC)，则p是f的一个蕴涵项。如在上面例子中({x’z}subseteq ON)。注意上述包含关系实质上为布尔代数上的偏序关系，(p subseteq f iff p preceq f)。下文将大量应用布尔代数的一些性质和定理而不加说明。

　　显然有(ON subseteq sum_{pin f}p)，即f的所有蕴涵项盖住了f=1的全部最小项，且根据定义(OFF notsubset sum_{pin f} p)，即不盖住f=0的最小项f。

　　如果p是f的蕴涵项，且f不存在其它的蕴涵项(p’)满足(p subseteq p’)，p’具有更少的文字，那么p同时也是f的素蕴涵项。

2.2 Quine-McCluskey算法原理

　　下面证明定理1：
设与(E)等价的SOP表达式为(Phi)，(Phi)的每个子句为(e)，且(mathcal{L}(sum_{e subseteq Phi} e))取最小值。
显然(esubseteq Phi)，(esubseteq E)。
如果(Phi)的子句中存在e不是素蕴涵，则存在(bsubseteq Phi)，满足(e subseteq b)，b文字数小于等于e。
所以存在(varphi=(Phi-{e})cup b)，(mathcal{L}(sum_{b subseteq varphi} b) ，与假设矛盾
所以e必须是E的素蕴涵。
Q.E.D

　　可见算法的最优性是由素蕴涵的定义保证的，如何计算所有符合定义的素蕴含项就成为核心问题。我们在下一节证明一些引理后就可以设计出枚举素蕴涵的算法。

　　暂时回到整个化简算法，定理1给出了最优解的必要条件，因此只需在所有素蕴涵项(P)中找解。显然最优解(M subseteq P)满足如下条件：

（1）(M)与原始函数逻辑等价，即(ON subseteq M subseteq (ON cup DC))

（2）(mathcal{L}(sum_{p in M} p))取最小值。

　　子集(M)的选择是一个组合优化问题。稍后的分析将看到，其本质为集合覆盖问题（SCP）。

3 Quine枚举素蕴涵项

　　Quine利用如下性质和定理计算蕴涵项：

并项法：xy + x’y = y

定理3：y是xy + x’y的蕴涵项

　　证明：
(y是xy + x’y的蕴涵项)
(iff y preceq xy + x’y)
(iff y(xy + x’y)’ = bf{0})
(iff yy’ = bf{0})
Q.E.D

　　定理3表明，对相邻两项（仅相差一对互补的变元）之和应用并项法可以导出一个蕴涵项。

　　然而定理3中的蕴涵项不一定是素蕴涵项，如下定理用于计算素蕴涵项：

定理4：如果函数f的一对蕴涵项a、b可根据并项法产生新的蕴涵项c，则a、b不是素蕴涵项。

　　证明：
由布尔代数性质：
(a preceq a + b)
(b preceq a + b)
又蕴涵项c是由a、b并项产生的，即(c = a + b)
所以(a preceq c)且(b preceq c)
因为a、b是f的蕴涵项，(a preceq f)、(b preceq f)
所以(a + b preceq f)，即(c preceq f)
所以函数f存在另一个蕴涵项c，且满足(a preceq c)且(b preceq c)。
因为并项法结果必然少1个文字，所以c的文字少于a、b。
上述两条结论与素蕴涵项的定义矛盾，所以a、b不是素蕴涵项
Q.E.D.

根据定理4，可设计一种基于筛选的算法，从一组蕴涵项T中求素蕴涵：

• P1 [并项] 如果存在(a,b in T)满足定理4的条件，标记a、b，把c加入T
• P2 重复P1直到无蕴涵项可加入
• P3 未被标记的蕴涵项一定是素蕴涵项。

　　算法中如果a、b可以并项，不能删除a、b，而要继续跟其它项合并。设想如果删除了a、b，就会丢失只有与a、b并项才能得到的蕴含项。这与本文一开始提到的迭代算法有所不同。

　　注意到布尔函数f的所有最小项都是蕴涵项，以这些蕴涵项为初始的T，运用上述算法可计算出f的所有素蕴涵项。

　　因为所有最小项构成原子，合并原子所得素蕴涵项没有遗漏，结果是完备的。

上述算法的P2蛮力实现需要(O(n^2))时间。经过简单优化后，得到Quine求素蕴涵的算法：

　　算法中只需相邻两个分组比较，因为不相邻的分组必不可合并。

　　下面举一些实例。

例1：Quine算法计算f=x’y’z’+x’zw’+xy’zw’+xy’z’的素蕴涵项
香农展开得到最小项表达式f=x’y’z’w’ + x’y’z’w + x’y’zw’ + x’yzw’ + xy’z’w’ + xy’z’w + xy’zw’
分组、迭代计算过程如下：

	最小项 + 标记	1次迭代 + 标记	2次迭代 + 标记
第0组	x’y’z’w’ √
第1组	x’y’z’w √ x’y’zw’ √ xy’z’w’ √	x’y’z’ √ x’y’w’ √ y’z’w’ √
第2组	x’yzw’ √ xy’z’w √ xy’zw’ √	y’z’w √ x’zw’ y’zw’ xy’z’ √ xy’w’ √	y’z’ y’w’

未标记√的项：x’zw’、y’zw’、y’z’、y’w’即为所有素蕴涵项。

　　上述算法未考虑含无关项的情况。下面扩展上述算法使其能够处理无关项：单独标记无关项，当用并项法合并a、b两项时，如果a、b都标记为无关项，那么结果c也标记为无关项。最后所有标记了d的素蕴涵项都可以丢弃。

例2：Quine算法计算f=yz’+xy’z（无关项d=x’z）的素蕴涵项

	最小项 + 标记	1次迭代 + 标记
第0组	x’yz’ √ x’y’z √ d
第1组	x’yz √ d xyz’ √ xy’z √	x’y yz’ x’z d y’z

未标记√和d的项：x’y、yz’、y’z即为所有素蕴涵项。

4 集合覆盖生成最小SOP

　　Quine方法计算出了函数f的所有素蕴涵项(Psubseteq (ON cup DC))。回顾3.2，为了生成最小SOP，我们要选出P的一个子集M，该子集要满足(ON subseteq M subseteq (ON cup DC))，同时代价函数(mathcal{L}(sum_{p in M} p))要最小化，这是一个组合优化问题。

　　下面以例1说明该问题。

　　上面覆盖矩阵的行对应最小项，列对应素蕴涵项，矩阵元素(a_{ij}=1)表示第j个素蕴涵项盖住第i个最小项（事实上只需满足素蕴涵项j的所有文字都包含在最小项i中。这里粗略证明：设素蕴涵项为p，最小项为m。假设m=1，则m中每个文字=1，又因为p的所有文字都包含在m中，所以p的每个文字=1，所以p=1，所以(m Rightarrow p)，所以(m preceq p)）。

　　为了满足(ON subseteq M)，我们需要恰当选取一些列，使得这些列构成的矩阵每一行都至少有一个1。例如选择列x’zw’、y’z’和y’w’构成如下矩阵：

　　这个例子中矩阵每行都至少有一个1，这意味着所有最小项都至少被一个选定的素蕴涵项盖住，即(ON subseteq {x’zw’, y’z’, y’w’})，所以选择M={x’zw’, y’z’, y’w’}是可行的。

　　为了最小化代价函数(mathcal{L}(sum_{p in M} p))，选择的列应尽可能少；当存在多种列数相同的方案时，应优先选择文字数少的方案。例1只有唯一可行解，代价函数(mathcal{L}(x’zw’ + y’z’ + y’w’) = 10)，最小SOP表达式为x’zw’ + y’z’ + y’w’。

　　问题本质上是集合覆盖问题（SCP），该问题是NP-hard的。求解SCP的方法主要有分支限界法（保证最优性）和启发式算法，涉及大量剪枝和优化方法，本文无法一一列举。

　　这里说一种新的求解思路：将SCP编码为Max-SAT问题。

4.1 Max-SAT问题

　　SAT问题是说判断CNF表达式的可满足性。若存在真值指派使表达式为1（即CNF的所有从句都满足），则CNF是可满足的；如果这组值不存在，则判定为不可满足（可证伪的）。
　　Weighted Partial Max-SAT（WPMS）是SAT的变种，将CNF表达式中的子句分成软/硬子句，要求所有硬子句都满足，同时最小化不满足的软子句的权重之和，属于优化问题。

4.1.1 SCP的Max-SAT编码

1. 变元：(forall p in P)，定义变元(v_p=0)表示素蕴含项p不包含在答案M中，(v_p=1)表示素蕴含项p包含在M中。
2. 硬子句：(forall m in ON)，添加硬子句({v_p|msubseteq p,p subseteq P})，保证所有最小项都至少被一个选定的素蕴涵项盖住。
3. 软子句：(forall p in P)，添加软子句(neg p)，设置权重(w(p)=p中文字的个数)。

求解上述问题，得变元赋值v0,v1,v2,…,vi，对应第i个素蕴含项是否被选中。

4.1.2 求解

　　最近的2022 MaxSAT Evaluation结果可在https://maxsat-evaluations.github.io/2022/rankings.html查看，代表了SAT求解器的SOTA。
　　MaxSAT的求解并不是本文重点，直接调用Loandra求解器。

4.2 Loandra求解实例

　　第3节中的例1，将Quine算法得到的素蕴含项(x’zw’, y’zw’, y’z’, y’w’)分别编号1 2 3 4，按4.1.1节所述编写CNF文件如下：

c QM logic simplify
h 3 4 0
h 3 0
h 1 2 4 0
h 1 0
h 3 4 0
h 2 4 0
3 -1 0
3 -2 0
2 -3 0
2 -4 0

　　(h表示硬子句，0表示输入结束，数字开头的行表示软子句的权重，-号表示否定(neg))

执行./loandra input.txt，得到求解结果：

c ========================================[ Problem Statistics ]===========================================
c |
c |  Problem Format:             MaxSAT
c |  Problem Type:             Weighted
c |  Number of variables:             4
c |  Number of hard clauses:          6
c |  Number of soft clauses:          4
c |  Number of cardinality:           0
c |  Number of PB :                   0
c |  Parse time:                   0.00 s
c |
o 7
s OPTIMUM FOUND
v 1011

　　loandra给出的解为1011，对应每个素蕴含项是否可取，因此化简结果为(x’zw’ + y’z’ + y’w’)。

参考

[1] C. E. Shannon, “A symbolic analysis of relay and switching circuits,” in Electrical Engineering, vol. 57, no. 12, pp. 713-723, Dec. 1938, doi: 10.1109/EE.1938.6431064.
[2] Quine, W. V.. “The Problem of Simplifying Truth Functions.” American Mathematical Monthly 59 (1952): 521-531.

服务器托管，北京服务器托管，服务器租用 http://www.fwqtg.net
机房租用，北京机房租用，IDC机房托管， http://www.e1idc.net