轉載請務必注明出處：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形式的邏輯化簡。之所以希望輸出仍然是兩級邏輯，是因為兩級邏輯具有特定優勢，例如物理結構規則，傳播延遲低等，過去常見於可編程邏輯器件中。
2 Quine-McCluskey兩級邏輯化簡
一些概念：
變元：x1,x2,...xn
文字：變元或其否定：x1, x1',...
子句（乘積項、項）：不重復文字的合取：x1x2, x1'x2,...
邏輯化簡本質上是對表達式進行等價轉化以最小化代價函數的優化過程，其中代價函數評估了表達式的優劣（如對應電路的PPA）。定義SOP表達式E的代價函數為：
給定布爾函數f，\(\arg\min\limits_{E=f} \mathcal{L}(E)\)即為兩級邏輯化簡的結果，其中E必須是SOP表達式。
\(\arg\min\limits_{E=f} \mathcal{L}(E)\)具有最小的電路面積，這是因為E的子句的個數決定第二級邏輯(OR)的面積，文字的個數決定第一級邏輯(AND)的面積。
我們熟知的卡諾圈數量越少，則對應子句越少；卡諾圈面積越大，則消去的文字約多。但卡諾圖對於高維函數顯得無能為力，在工程應用中失去價值。其實卡諾圖中最大的圈本質上對應素蘊涵項。素蘊涵項是兩級邏輯化簡的核心概念。要理解這個概念，需要一些前置知識，之后我們將結合Quine[2]證明：
定理1：代價函數\(\mathcal{L}(E)\)定義的最小SOP表達式一定是素蘊涵項之和
這定理對搜索空間做出了限定：只需在E的素蘊涵項的組合中搜索最小代價即可。這就是Q-M的核心思想。至於如何搜索，Quine在[2]中提出了一種做法。但本文后面可以看到，該問題可以轉化為很多其它常見的問題形式，如SCP、Max-SAT等等，利用現代優化過的SOTA求解器解決。
2.1 蘊涵項與素蘊涵項
蘊涵項、素蘊涵項、最小化素蘊涵項等術語的定義在不同文章中有區別，會造成討論上的誤解，因此必須在此明確。
首先需要明確ON/OFF集與無關DC集（Don't care set）的概念。邏輯函數\(f: \{0,1\}^n \rightarrow \{0,1,*\}\)，其中\(*\)表示無關位（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'}。
定義\(\preceq\)為布爾代數\(B(;+,*,\bar{\space},0,1)\)上的偏序關系，\(x \preceq y\iff x\rightarrow y\iff\)使x為真的變元取值代入y結果為真。給定函數f和子句p，如果\(p \preceq ON \cup DC\)，則p是f的一個蘊涵項。顯然f的蘊涵項p必不滿足\(p \preceq OFF\)。f的所有蘊涵項之和與f邏輯等價。
例如，f的所有最小項都是它的蘊涵項。又如，上面例子中\(\{x'z\}\preceq ON\)是f的一個蘊涵項，因為若x'z=1，則變元x=0，z=1，則ON的子集{x'y'z, x'yz}=1。還要強調蘊涵項一定是子句，這與布爾代數中討論的蘊涵有明顯區別，例如2元布爾代數中\(xy+x'y'\preceq x'+y\)，但\(xy+x'y'\)不是子句。
如果p是f的蘊涵項，且f不存在其它的蘊涵項\(p'\)滿足：\(p \preceq p'\)，且p'具有比p更少的文字，那么p同時也是f的最小化素蘊涵項，本文簡稱素蘊涵項。也就是說，任何一個素蘊涵去掉任意文字都導致非蘊涵。
現在能理解為什么在卡諾圖中，如果一個圈不可能被其他更大的圈包含，則該圈就對應素蘊涵項。因為假設圈c被更大圈c'的包含，則c'對應表達式\(\preceq\)c，且c'具有比c更少的文字（c’能消去更多文字），與素蘊涵矛盾。直觀上講，如果f的一個蘊涵項p不是素蘊涵，則有可能通過刪除p中的一個文字，將p變為素蘊涵，並項法可以實現這種刪除，這也是之后要介紹的。
2.2 Quine-McCluskey算法原理
下面證明定理1：
設SOP表達式為\(\Phi\)，\(\Phi\)的每個子句為\(e\)，且\(\mathcal{L}(\sum_{e \subseteq \Phi} e)\)取最小值。
顯然\(e\preceq \Phi\)。
如果\(\Phi\)的子句中存在e不是素蘊涵，則存在\(b\preceq \Phi\)，滿足\(e \preceq b\)，b文字數小於等於e。
所以存在\(\varphi=(\Phi-{e})\cup b\)，\(\mathcal{L}(\sum_{b \subseteq \varphi} b) < \mathcal{L}(\sum_{e \subseteq \Phi} e)\)，與假設矛盾
所以e必須是E的素蘊涵。
Q.E.D
例如，f=xy'+y，已知x是xy'關於f的素蘊涵，則可以通過將xy'替換為x，得到f=x+y，減少一個文字，得到更優結果。
如何計算所有符合定義的素蘊含項就成為接下來的問題。我們在下一節證明一些引理后就可以設計出枚舉素蘊涵的算法。現在已經有了算法的全貌。定理1給出了最優解的必要條件，因此只需在所有素蘊涵項\(P\)中找解，即解決如下組合優化問題：
s.t. (1). \(M\subseteq P\)
(2) \(ON \subseteq M \subseteq (ON \cup DC)\)，即\(M\)與原始函數邏輯等價
稍后的分析將看到，可以把這個問題等價轉換為集合覆蓋問題（SCP）、Max-SAT等等問題形式來求解。
3 Quine枚舉素蘊涵項
Quine在原始論文[2]中的THEOREM 2~4說明了列舉素蘊涵項的原理，通過定義subsume和completion的概念完成了證明。為了不引入新的概念，本文提供一種新的角度，從熟知的並項法的角度給出證明。
顯然布爾函數f的所有最小項都是f的蘊涵項。對相鄰最小項使用並項法：
性質1：並項法：\(y \preceq xy + x'y\)
這表明相鄰兩項（僅相差一對互補的變元）應用並項法可以導出一個新的蘊涵項，並且少一個文字。然而蘊涵項不一定都是素蘊涵項，如下兩個引理用於計算素蘊涵項：
引理1：如果對於函數f的蘊涵項a，存在f的蘊涵項b，使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)
又因為並項法結果必然少1個文字，所以c的文字少於a、b ......(2)
(1)、(2)與素蘊涵項的定義矛盾，所以a、b不是素蘊涵項
Q.E.D.
引理2：若函數f的蘊涵項\(a\)不是函數f的素蘊涵項，則存在f的蘊涵項\(b\)，a、b可以根據並項法產生新的蘊涵項c
證明：
已知\(a \preceq f\)，且a不是素蘊涵項
則由素蘊涵定義可知 \(\exist a'\preceq f且a'\ne a\), 使\(a=a'\zeta\)
其中\(\zeta\)是屬於a而不屬於a'的非空文字串
因為\(a'\bar{\zeta}\preceq a' \preceq f\)
即\(a'\bar{\zeta}\)是f的一個蘊涵項
所以存在\(b=a'\bar{\zeta}\)，使得\(a+b=a'\zeta+a'\bar{\zeta}=a'\)
Q.E.D.
根據引理1、2，推出：
定理2 函數f的蘊涵項a不是素蘊涵項的充分必要條件是，存在f的蘊涵項b，使a、b可以根據並項法產生新的蘊涵項。
據此可設計一種基於篩選的算法，對於f的每一個蘊涵項，驗證是否存在另一個蘊涵項可以與它並項，若能則排除該非素蘊涵項，最終排除所有非素蘊涵項：
- P0 輸入f，展開f的所有最小項加入T中
- P1 如果存在\(a,b \in T\)可以並項為c，則標記a、b，把c加入T
- P2 重復P1直到無蘊涵項可加入
- P3 輸出未被標記的項（素蘊涵項）。
注意到算法中如果a、b可以並項，不刪除a、b，而要繼續跟其它項合並。設想如果刪除了a、b，就會丟失只有與a、b並項才能得到的蘊含項，從而漏解。
上述算法中還有一個重要問題，為什么從函數f的所有最小項出發，可以求出f的所有素蘊涵項？（暫時不考慮無關項）
定理3 f的蘊涵項的所有文字一定包含在f的某個最小項中
證明：
假設f的蘊涵項p的所有文字不包含在f的所有最小項\(m_i\)中
由最小項定義，\(m_i\)包含f的所有變元。
則\(m_i\)和p必然包含互補的文字，即\(m_i=m'_i\xi\)，\(p=p'\bar\xi\)。
則p=1時，\(\xi=0\)，\(m_i=0\)
則\(p \preceq m_i\)不成立，與p是蘊涵項矛盾。
Q.E.D
這說明蘊涵項只能從最小項刪除部分文字產生。由性質1，刪除k>1個文字等價於對兩個從最小項刪除k-1個文字得到的相鄰蘊涵項運用並項法，即對2^k個相鄰最小項運用並項法。因此算法P1步能不斷生成新的蘊涵項，同時利用定理2排除非素蘊涵。當算法步P2跳出循環后，T中一定包含所有蘊涵項/素蘊涵項。
上述算法的P2中，蠻力實現需要兩兩比較蘊涵項，其實對子句排序（分組）后再相鄰比較就可以，這就導出了優化后的算法：
算法1：求所有素蘊涵項 |
|---|
| 輸入：ON：f=1的所有最小項 |
| 輸出：PI：素蘊涵項集合 |
| 1. 將ON中的子句按反變元（變元的補）的個數分組，沒有出現反變元的項歸為第n組、有1個反變元的項為n-1組、……、有n個反變元的項為第0組。對於反變元個數相同的子句，再按變元的字典序排序。 |
| 2. 依次比較相鄰兩組（第\(i\)和\(i+1\)組的每一對子句（從第\(i\)組選擇一個子句，再從第\(i+1\)組選擇一個子句構成一對）。如果這對子句僅一個文字不同（形如xy與x'y），則標記這兩項，根據並項法生成一個蘊涵項y。 |
| 3. 迭代處理：如果步驟2生成了一些蘊涵項，令ON為新生成的蘊涵項構成的集合，轉到1；如果不再生成任何蘊涵項，結束。 |
| 經過上述步驟，所有未被標記的子句就是素蘊涵項。 |
下面舉一些實例。
例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的所有素蘊涵項\(P\subseteq (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個素蘊涵項\(\preceq\)第i個最小項。然而直接判斷\(\preceq\)關系比較困難，下面要證明一個定理以簡化判斷。
定理4：如果子句p的所有文字都包含在子句m中，則\(m \preceq p\)。
證明：
假設m=1，則m中每個文字=1
已知p的所有文字都包含在m中，所以p的每個文字=1
所以p=1
所以\(m \preceq p\)
Q.E.D
因此可以通過字符串包含關系判斷第j個素蘊涵項的所有文字是否都包含在第i個最小項中，若包含則\(a_{ij}=1\)。
為了滿足\(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'。
4.1 集合覆蓋
仔細將上述問題與集合覆蓋問題（SCP）對比，就會發現兩者是等價的。SCP問題是NP-hard的，因此上述問題也是NP-hard的。
求解SCP的方法主要有分支限界法（保證最優性）和啟發式算法，涉及剪枝等大量Ad-hoc技術，本文無法一一列舉。
4.2 Max-SAT
這里再說一種求解思路：將生成最小SOP問題轉換為Max-SAT。
很多組合優化問題都可以編碼成Max-SAT問題。SAT問題是說判斷CNF表達式的可滿足性。若存在真值指派使表達式為1（即CNF的所有從句都滿足），則CNF是可滿足的；如果這組值不存在，則判定為不可滿足（可證偽的）。
Weighted Partial Max-SAT（WPMS）是SAT的變種，將CNF表達式中的子句分成軟/硬子句，要求所有硬子句都滿足，同時最小化不滿足的軟子句的權重之和，屬於優化問題。
4.2.1 生成最小SOP的問題編碼
- 變元：\(\forall p \in P\)，定義變元\(v_p=0\)表示素蘊含項p不包含在答案M中，\(v_p=1\)表示素蘊含項p包含在M中。
- 硬子句：\(\forall m \in ON\)，添加硬子句\(\{v_p|m \preceq p,p \subseteq P\}\)，保證所有最小項都至少被一個選定的素蘊涵項蓋住。
- 軟子句：\(\forall p \in P\)，添加軟子句\(\neg p\)，設置權重\(w(p)=p中文字的個數\)。
求解上述問題，得變元賦值v0,v1,v2,...,vi，對應第i個素蘊含項是否被選中。
4.2.2 求解器
最近的2022 MaxSAT Evaluation結果可在https://maxsat-evaluations.github.io/2022/rankings.html查看，代表了SAT求解器的SOTA。
MaxSAT的求解並不是本文重點，直接調用Loandra求解器。
4.2.3 求解實例
第3節中的例1，首先運行Quine算法，得到素蘊含項\(x'zw', y'zw', y'z', y'w'\)。
接下來調用Loandra求解SCP，設編號1 2 3 4的CNF變量的含義是對應素蘊含項是否被選取，按4.1.1節所述編寫CNF文件如下：
c WPMS
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，對應滿足CNF的各變量的一組取值。按照上文變量假設，可知化簡結果為\(x'zw' + y'z' + y'w'\)。
5 時間復雜度
Quine的主要時間消耗在最小項生成。利用香農展開n變量布爾函數，最壞時間為\(O(2^n)\)。而生成最小SOP最壞時間為\(O(2^n)\)。總時間隨變量個數n增加呈指數級增長。
參考
[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.