Pruning Boolean d-DNNF Circuits Through Tseitin-Awareness

基于 Tseitin 感知的布爾 d-DNNF 電路剪枝方法

https://arxiv.org/abs/2407.17951?

摘要

以d-DNNF形式表示的布爾電路能夠實現可處理的概率推理。然而，作為本研究的一個關鍵發現，我們表明常用的d-DNNF編譯方法引入了無關的子電路。我們將這些子電路稱為Tseitin偽影（Tseitin artifacts） ，因為它們是由于Tseitin變換 步驟所引入的——這是一種將任意電路轉換為CNF格式的經典過程，而CNF是許多d-DNNF知識編譯器所必需的輸入格式。我們討論了如何檢測并移除Tseitin變量和Tseitin偽影，從而得到更簡潔的電路。實驗觀察表明，在移除Tseitin變量和偽影后，電路大小平均減少了77.5%。進一步去除Tseitin偽影又平均減少了22.2%的大小。這一優化顯著提升了受益于更緊湊電路的下游任務，例如概率推理任務。

關鍵詞 —知識表示形式與方法

I. 引言

布爾電路以一種允許執行某些操作的方式表示布爾函數。在本文中，我們重點關注d-DNNF電路 （見圖1中的示例），因為盡管加權模型計數（weighted model count）在一般情況下是一個計算上困難的問題 [1]，但使用d-DNNF電路可以在多項式時間內完成這一任務。因此，它們在實現可處理的概率推理 中起著重要作用 [2]–[7]。

此外，采用電路方法來計算加權模型計數的一個關鍵優勢是：當權重發生變化時，可以重復使用已編譯的電路，只需重新執行電路評估。這有效地將編譯成本分攤到多次評估中，在參數學習等需要多次評估的場景中尤為重要，因為在這些場景中參數會隨著多次迭代不斷變化。然而，在這種背景下，電路的大小也變得至關重要。例如在神經符號人工智能 （neuro-symbolic AI）中，這類電路與神經網絡結合使用，在訓練過程中會進行大量評估，高效的電路評估對于保持足夠快的神經網絡學習流程至關重要 [8], [9]。

總之，除了高效地獲得d-DNNF電路外，確保這些電路的簡潔性 （succinctness）也很重要。

為了從任意布爾電路中獲得簡潔的d-DNNF電路，知識編譯 （knowledge compilation）領域開發了多種d-DNNF編譯器。其中基于CDCL的一類編譯器，包括D4 [10] 和 sharpSAT-TD [11]，要求輸入電路必須為合取范式 （CNF）。為了高效地將電路轉換為這種形式用于編譯，最著名的算法是Tseitin變換 [12]。這是一種將任意命題級布爾電路ψ轉換為與其等可滿足性的CNF形式的方法。

Tseitin變換的一個副作用是它會引入額外的輔助變量。這些變量可以通過存在量詞消去 （existential quantification）在編譯后被移除 [11]。然而，作為本文的主要貢獻之一，我們提出一個關鍵見解：這種方法可能會導致永真型d-DNNF子電路 （tautological d-DNNF subcircuits）的產生。也就是說，這些子電路等價于“真”（true），可以完全刪除。我們將這些子電路稱為Tseitin偽影（Tseitin artifacts），因為它們是在Tseitin變換之后的編譯過程中產生的。我們在第三節中對這類偽影進行了討論并給出了正式定義。

通過一次自底向上的遍歷過程，可以高效地在已編譯的d-DNNF電路中檢測出Tseitin偽影。我們在第四節中詳細討論了這種方法，并分析了這些偽影通常會在什么情況下出現。隨后在第五節中簡要回顧相關工作。最后，在第六節中，我們通過實驗證實了Tseitin偽影的普遍存在性，并展示了主動移除Tseitin變量和Tseitin偽影后，電路大小平均減少了77.5% 。與僅移除Tseitin變量相比，進一步去除Tseitin偽影又平均減少了22.2%的電路大小（如果只考慮確實存在Tseitin偽影的電路，則平均減少 29.7% ）。

II. 背景知識 A. 命題邏輯

我們使用標準的命題邏輯術語。

B. 加權模型計數

定義1（加權模型計數） ：給定一個在變量集 V 上的命題公式 ψ，以及一個權重函數 w，該函數將每個文字映射到一個實數值，則加權模型計數 （Weighted Model Count, 簡稱 WMC）定義為：

當變量集 V 可以從上下文中明確得知時，我們將使用記號 WMC(ψ,w)；而用 MC(ψ) 表示無權重模型計數（unweighted model counting），即對所有文字賦予權重 1 的情況。

由于概率推理可以被轉化為一個加權模型計數 （WMC）任務 [2], [13]，因此高效地計算 WMC 具有重要意義。使用基于編譯的方法可以實現這一目標。

C. 電路性質

D. CDCL 算法

已有多種算法被提出，用于將布爾電路編譯為 d-DNNF 形式。許多最先進的編譯器基于 CDCL（沖突分析學習驅動子句）算法 ，該算法最初是為求解 SAT 問題而設計的，但也可以被改編用于知識編譯。這類編譯器的例子包括 D4 [10]和 sharpSAT-TD [11], [16] 。關于這些算法的詳細說明，我們參考文獻 [10]、[11] 和 [17]。

理解我們工作的關鍵在于：這些算法操作于一個 CNF 公式 ψ，并通過迭代地對文字進行條件限制，直到剩余的公式被滿足為止。

例2 ：考慮以下公式 ψ，它是一個包含兩個子句的 CNF 公式：

另一個相關的重要技術是組件分解 （component decompositioning） [18]，這是在加權模型計數和 d-DNNF 編譯中廣泛使用的一種非常有效的優化方法，用于減少搜索空間。該優化利用了如下事實：如果一個 CNF 公式可以劃分為若干互不共享變量的子句集合（稱為組件 ），那么這些組件可以被分別處理。此外，這些組件可以被緩存，當它們在搜索空間的其他部分再次出現時，可以直接復用緩存的結果。對于 d-DNNF 編譯來說，這使得子電路得以重復使用，從而生成的是一個有向無環圖 （DAG），而非一棵樹。

這一優化的有效性促使研究社區提出了多種組件表示方式 [19]–[21]。

例3 ：考慮以下由三個子句組成的 CNF 公式：

同樣，在 d-DNNF 編譯中，這兩個組件也可以分別進行編譯，然后通過合取（∧）組合起來。

基于 CDCL 的編譯算法要求輸入公式 ψ 是一個 CNF 公式，這可以通過使用 Tseitin 變換 來獲得。

E. Tseitin 變換

Tseitin （或 Tseytin ）變換是一種可以將任意布爾電路 ψ 轉換為合取范式（CNF）的過程 [12]。

III. 什么是 Tseitin 偽影（Tseitin Artifacts）？

我們首先非正式地介紹我們所稱的 Tseitin 偽影 （Tseitin artifact），隨后再給出更正式的定義。我們在 d-DNNF 編譯 的背景下研究這些偽影。因此，假設我們希望獲得例4中電路 ψ（公式4）的一個 d-DNNF 表示。我們將使用一個基于 CDCL 的 d-DNNF 編譯器，而它要求輸入為 CNF 形式。因此，我們首先使用 Tseitin 變換 來得到 T(ψ)（公式6）。

圖1展示了編譯器可能輸出的一個結果：一個表示 T(ψ) 的 d-DNNF 電路。由于我們關注評估過程中的計算次數，我們將電路的大小定義為二元節點的數量（例如，一個有三個輸入的節點代表兩個二元節點，依此類推）。圖1中 d-DNNF 的大小為 16。

A. Tseitin 變量的存在量詞消去

圖1中的電路是一個 d-DNNF，因此可以用于高效計算 T(ψ) 和 ψ 的加權模型計數。然而，當前的表示中包含了許多不必要的元素。特別是，Tseitin 變量 X 是為了方便地獲得 CNF 而由 Tseitin 變換引入的，它們對后續的計數任務并不重要。這些變量可以通過存在量詞消去 （existential quantification）移除，即通過計算 ?X.T(ψ)。

得益于可分解性（decomposability）性質，在此情況下對 X∈X 進行存在量詞消去非常簡單：只需將公式中所有 x 和 ?x 替換為 ?。我們將這一過程稱為 EXISTS(ψ, X) 。該過程能保證保留 DNNF 性質 [22]。此外，最近的研究表明，由于我們是對 Tseitin 變量進行存在量詞消去，該過程還能保證保留確定性（determinism） [11]。

圖2展示了在對 Tseitin 變量執行存在量詞消去后，圖1中電路的結果。結合上述結論與公式（7）可知，圖2再次表示的是電路 ψ 而不是 T(ψ)，但由于之前的編譯步驟，現在它是以 d-DNNF 的形式表示的。

IV. 檢測 Tseitin 偽影 A. 如何檢測它們？

Tseitin 偽影可以在 sd-DNNF 表示中以與 sd-DNNF 大小成線性關系的時間被檢測出來。

眾所周知，每個 sd-DNNF （子）電路的模型計數可以在其表示大小的線性時間內計算出來，并且對于非平滑的 d-DNNF 表示，也可以通過在評估前或評估過程中以多項式時間執行適當的平滑操作來采用類似的方法 [1], [15]。此外，由于我們只需要無權重的模型計數，因此平滑并不是必需的，我們只需知道那些需要被平滑的變量數量即可。

這些所謂自由變量 （free variables）的數量在編譯過程中很容易提取。結合這一事實與命題1（Proposition 1），我們可以通過一次自底向上的遍歷，計算每個子電路 f(X,Y) 的無權重模型計數，從而檢測出 Tseitin 偽影。

如果該模型計數等于 ，則說明 f 是一個 Tseitin 偽影，并且在我們對變量 X 執行存在量詞消去時可以將其移除。

B. 它們何時會出現？

接下來，我們進一步解釋這些偽影在基于 CDCL 的 d-DNNF 編譯器中何時可能出現 。這有助于識別哪些類型的電路會從我們提出的技術（移除 Tseitin 偽影）中獲得顯著效果。

再次考慮例4中的電路 ψ 和其經過 Tseitin 變換后的形式 T(ψ)。

V. 相關工作

已有研究 [22] 探討了使用存在量詞消去（即 EXISTS 過程）來獲得更簡潔的 DNNF 電路的方法。在此基礎上，[11] 證明了如果變量集合 X 是由其他變量定義的，那么對 X 進行存在量詞消去也能保持確定性（determinism），因此這一方法也適用于目標為 d-DNNF 的編譯過程。我們的工作延續了這些發現，進一步意識到：該過程可能會引入可以被完全移除的子電路，從而進一步減小電路規模。

可定義性 （definability）的概念與 Tseitin 變量密切相關，此前已被用于預處理階段，以修改 CNF 來提升模型計數效率 [23], [26]。類似地，[11] 中提出的變量消去方法也可以在編譯前就消除 Tseitin 變量。雖然這在某些情況下是有益的，但在涉及 Tseitin 變量時也可能降低性能，因為這些變量正是為了確保較小的 CNF 規模（從而加快編譯速度）而被引入的 [11]。因此，他們考慮使用啟發式方法來決定哪些變量應該被消除。此外，在編譯之前提前消除 Tseitin 變量會阻止編譯器對這些變量進行條件限制，這可能導致更大的電路規模，并可能增加編譯時間。

[27] 提出了一種新的投影模型計數器 ，其僅限于處理 Horn 子句 ，這類子句的形式等價于，其中 是正文字或 ?。這項工作與我們研究的相關之處在于其所采用的傳播技術。該技術基于一個洞察：在計數過程中，如果 h 是一個輔助變量，并且沒有被任何剩余的 Horn 子句所約束，那么與之相關的子句可以在不影響計數的情況下被滿足。換句話說，這樣的子句可以被刪除（僅僅是因為 h 是一個輔助變量）。

這種方法與我們提出的 Tseitin 偽影有相似之處，盡管 Tseitin 偽影來源于等價結構而非蘊含結構，并且不局限于投影模型計數。

VI. 實驗

鑒于變量順序以及電路 ψ 中析取結構的影響，一個自然的研究問題是：Tseitin 偽影有多普遍？

我們主要關注前者，并避免選擇那些已知不會包含 Tseitin 偽影的實例（例如具有互斥析取結構的貝葉斯網絡）。我們研究移除 Tseitin 偽影對電路大小的影響，并比較僅執行簡單存在量詞消去（記為 d-DNNF+p）與完全移除 Tseitin 偽影（記為 d-DNNF+t）之間的效果差異。

A. 數據集

a) 反向工程獲得的 CNF（MCC） ：
用于加權模型計數和 d-DNNF 編譯的基準測試數據通常是已經以 CNF 形式提供的公式，因此從 Tseitin 變換的角度來看它們并不有用。然而，在我們的實驗中，我們假設這些 CNF 是在公開發布之前由 Tseitin 變換生成的。我們通過識別等價式來確定 Tseitin 變量集合 X。

我們使用的數據集是 2022 年和 2023 年模型計數競賽（MCC）[28], [29] 的 CNF 實例，但只保留其中 Tseitin 變量占比超過 25% 的實例。我們使用 D4 d-DNNF 編譯器 [10] 進行實驗，設置超時時間為 3600 秒，最終得到了 65 個成功完成的實例（去除重復實例后）。

b) 包含 Tseitin 變量的 CNF（CNFT） ：
我們也考慮了 [11] 中使用的數據集：“一組新基準，使用兩個工具將（概率）邏輯程序轉換為 CNF [30], [31]，基于概率邏輯程序設計的標準基準”。根據構造方式，他們的輔助變量完全由其他變量定義。

我們還加入了使用 ProbLog [13] 轉換的額外程序，例如來自 [32]、源自 [33] 的電力傳輸網絡。這兩個數據集分別產生了 146 個和 34 個實例（已排除超時情況）。

此外，我們還從神經符號人工智能（Neuro-Symbolic AI, NeSy）領域引入了一個知識圖譜任務——“Countries”：

“Countries 是一個知識圖譜，表示地球上國家與大洲之間的 locatedIn 和 neighborOf 關系” [34]。

該任務包含三個推理任務，對應生成三個析取范式（DNF）公式。雖然可以生成更多實例，但由于結構相似，預期結果不會有顯著差異。因此，我們僅考慮這三個 DNF 公式，并應用 Tseitin 變換得到對應的 CNF 公式及 Tseitin 變量集合 X。

B. 實驗結果

a) MCC 數據集 ：圖5展示了在移除 Tseitin 偽影并執行存在量詞消去后，剩余節點的相對數量。平均而言，這種方法可以剪枝掉 68.3% 的節點（標準差為 22.6%）。進一步通過檢測 Tseitin 偽影所帶來的額外剪枝效果（即 d-DNNF+p 與 d-DNNF+t 的對比）如圖6所示。這一方法在65個實例中改善了其中的 27 個實例 ，平均剪枝率為 24.0% （僅對這27個實例而言，標準差為 26.7%）。

b) CNFT 數據集 ：圖7展示了在移除 Tseitin 偽影并執行存在量詞消去后，剩余節點的相對數量。平均而言，這種方法可以剪枝掉 81.1% 的節點（標準差為 13.1%）。進一步通過檢測 Tseitin 偽影所帶來的額外剪枝效果（即 d-DNNF+p 與 d-DNNF+t 的對比）如圖8所示。這一方法在180個實例中改善了其中的 155 個實例 ，平均剪枝率為 30.6% （僅對這155個實例而言，標準差為 15.7%）。我們單獨在表I中列出了來自神經符號人工智能（NeSy）任務的三個實例。

c) 討論 ：總體實驗結果表明，對無關變量進行存在量詞消去具有重要意義，并且通過移除 Tseitin 偽影可以獲得進一步的電路大小縮減。正如前面所討論的，Tseitin 偽影并非出現在每一個電路中。這一點在圖8中有所體現，在 gnb 類別的電路中沒有觀察到進一步的縮減，說明這些電路中并未產生 Tseitin 偽影。我們提出假設，并手動驗證了若干析取結構：gnb 電路中的析取是互斥的。這支持了第 IV-B 節中的解釋：如果析取之間存在重疊，則更可能生成 Tseitin 偽影；而互斥的析取則很少導致偽影的出現。

對于其余電路，該方法的效果非常明顯，尤其是考慮到存在量詞消去和 Tseitin 偽影檢測的計算開銷非常低。

VII. 結論

Tseitin 變換 通過引入輔助變量來獲得一個較小的 CNF 電路。這些變量在完成 d-DNNF 編譯后可以很容易地被移除。然而，正如我們所展示的那樣，此時可能會出現一些被平凡滿足的子電路 （即 Tseitin 偽影）。幸運的是，我們可以通過對 d-DNNF 電路進行一次自底向上的遍歷，輕松地檢測并移除這類偽影。

我們通過實驗驗證了移除這些偽影對最終電路大小的積極影響。在未來的工作中，我們將研究如何在編譯過程中檢測并移除這些偽影，以進一步減少編譯時間。這需要設計一種新的檢測機制，因為當前的方法依賴于每個子電路已經被編譯完成的前提。

附錄 A 互斥析取

當一個貝葉斯網絡的條件概率表被編碼為使得每個析取（∨）都是互斥 的形式時，所產生的 Tseitin 偽影會很少。我們以其中一個概率表為例進行說明，如下所示的概率分布 P(C∣A,B)：

我們現在簡要討論其中一個為數不多的 Tseitin 偽影實例。

形成該偽影的子公式如下所示（為清晰起見，此處使用等價式而非 CNF 表示，并用 x 和 y 分別表示 Tseitin 變量和非 Tseitin 變量）：

原文鏈接：https://arxiv.org/abs/2407.17951?