基于SAT問題實(shí)例特性的端到端SAT求解模型

摘 要：當(dāng)前基于神經(jīng)網(wǎng)絡(luò)的端到端SAT求解模型在各類SAT問題求解上展現(xiàn)了巨大潛力。然而SAT問題難以容忍誤差存在，神經(jīng)網(wǎng)絡(luò)模型無法保證不產(chǎn)生預(yù)測誤差。為利用SAT問題實(shí)例特性來減少模型預(yù)測誤差，提出了錯(cuò)誤偏好變量嵌入架構(gòu)（architecture of embedding error-preference variables，AEEV）。該架構(gòu)包含錯(cuò)誤偏好變量嵌入調(diào)整算法和動(dòng)態(tài)部分標(biāo)簽訓(xùn)練模式。首先，為利用參與越多未滿足子句的變量越可能被錯(cuò)誤分類這一特性，提出了錯(cuò)誤偏好變量嵌入調(diào)整算法，在消息傳遞過程中根據(jù)變量參與的未滿足子句個(gè)數(shù)來調(diào)整其嵌入。此外，提出了動(dòng)態(tài)部分標(biāo)簽監(jiān)督訓(xùn)練模式，該模式利用了SAT問題實(shí)例的變量賦值之間存在復(fù)雜依賴關(guān)系這一特性，避免為全部變量提供標(biāo)簽，僅為錯(cuò)誤偏好變量提供一組來自真實(shí)解的標(biāo)簽，保持其他變量標(biāo)簽為預(yù)測值不變，以在訓(xùn)練過程管理一個(gè)更小的搜索空間。最后，在3-SAT、k-SAT、k-Coloring、3-Clique、SHA-1原像攻擊以及收集的SAT競賽數(shù)據(jù)集上進(jìn)行了實(shí)驗(yàn)驗(yàn)證。結(jié)果表明，相較于目前較先進(jìn)的基于神經(jīng)網(wǎng)絡(luò)的端到端求解模型QuerySAT，AEEV在包含600個(gè)變量的k-SAT數(shù)據(jù)集上準(zhǔn)確率提升了45.81%。

關(guān)鍵詞：布爾可滿足性問題；消息傳遞網(wǎng)絡(luò)；機(jī)器學(xué)習(xí)

中圖分類號：TP399 文獻(xiàn)標(biāo)志碼：A 文章編號：1001-3695（2024）11-025-3376-06

doi：10.19734/j.issn.1001-3695.2024.03.0096

End-to-end SAT assignment model based on instance related characteristics of SAT

Long Zhengrong， Li Jinlong^?， Liang Yonghao

（School of Computer Science amp; Technology， University of Science amp; Technology of China， Hefei 230026， China）

Abstract：Recently， the neural network-based end-to-end SAT solver shows great potential in predicting the solution of SAT instances. However， SAT solvers do not accept any error， and the prediction error of neural network-based models is not inevitable. Aiming at the problem of the SAT does not allow for errors， this paper proposed an error preference variable embedding adjustment algorithm and a dynamic partial label supervised training mode to reduce the model prediction error by exploiting the properties of the SAT instance. Firstly， to take advantage of the characteristic that the more unsatisfied clauses a variable participates in， the more likely it was to be misclassified， this paper proposed an error preference variable embedding adjustment algorithm， which was used during the message passing process to adjust the embedding of a variable according to the number of unsatisfied clauses it participates in. In addition， this paper proposed a dynamic partial label supervised training mode， which exploited the feature of complex dependencies among variable assignments for SAT instances， avoiding to provide labels for all the variables， and providing only a set of labels from a solution for the error-preference variables， and keeping the other variables’ label as the predictions unchanged， which managed a smaller search space during the training. Finally， this paper presented experimental validation on 3-SAT， k-SAT， k-Coloring， 3-Clique， SHA-1 pre-image attack， and the collected SAT competition dataset. The results show that compared to the SOTA end-to-end model QuerySAT， AEEV improves the accuracy by 45.81% on the k-SAT dataset with 600 variables.

Key words：

Boolean satisfiability problem（SAT）; message passing neural network; machine learning

0 引言

布爾表達(dá)式的可滿足問題（SAT）是計(jì)算機(jī)科學(xué)領(lǐng)域的一個(gè)經(jīng)典問題^［1］?，F(xiàn)實(shí)世界中大量的調(diào)度、配置和優(yōu)化問題都可以建模為SAT問題，例如電路邏輯等價(jià)性檢查問題^［2～4］、形式化驗(yàn)證^［5～8］、密碼學(xué)^［9，10］等。因此，找到一個(gè)高效的SAT求解器十分有意義。

一個(gè)布爾表達(dá)式通常是由一系列變量{x_i}ⁿ_i=1∈{true（1），1（0）}和三個(gè)邏輯運(yùn)算符{與（∧）、或（∨）、非（?）}組成的。布爾表達(dá)式的可判定問題也就是判定是否存在一組變量賦值，使得布爾表達(dá)式的運(yùn)算結(jié)果為真。過去，許多人嘗試使用各種軟硬件方法來求解SAT問題^{［11～14］}。隨著近些年機(jī)器學(xué)習(xí)的快速發(fā)展，一些工作開始嘗試用神經(jīng)網(wǎng)絡(luò)來解決組合優(yōu)化問題^{［15～19］}，其中包括SAT?；谏窠?jīng)網(wǎng)絡(luò)的端到端求解模型通常將SAT實(shí)例轉(zhuǎn)換為圖表示，SAT實(shí)例中的變量和子句成為了圖中的節(jié)點(diǎn)，通過在圖上應(yīng)用神經(jīng)網(wǎng)絡(luò)模型來提取變量節(jié)點(diǎn)的嵌入，并使用二分類算法對將變量嵌入分為true或者1來得到SAT實(shí)例的一組解。然而，在其他機(jī)器學(xué)習(xí)的分類任務(wù)中誤差是可以接受的，基于神經(jīng)網(wǎng)絡(luò)的端到端SAT求解模型難以容忍誤差存在。對于一個(gè)SAT實(shí)例，只有正確分類其全部變量，才會(huì)使這個(gè)問題滿足。因此，避免SAT實(shí)例中的變量被錯(cuò)誤分類是用機(jī)器學(xué)習(xí)方法求解SAT問題的一個(gè)重要挑戰(zhàn)。

當(dāng)前基于神經(jīng)網(wǎng)絡(luò)的端到端求解模型通常利用SAT問題實(shí)例特性來減少預(yù)測誤差^{［20～23］}。NeuroSAT^［20］設(shè)計(jì)了一種特殊的消息傳遞網(wǎng)絡(luò)來利用SAT問題實(shí)例的結(jié)構(gòu)特性以減少預(yù)測誤差，但模型可求解的問題規(guī)模較小。QuerySAT^［21］則利用了SAT問題難以求解而易于驗(yàn)證這一特性，為每一輪消息傳遞之后的變量賦值進(jìn)行可滿足性驗(yàn)證并計(jì)算一個(gè)反映當(dāng)前賦值質(zhì)量的查詢值，最后將這個(gè)查詢值作為消息傳遞網(wǎng)絡(luò)的一個(gè)輸入。本文對消息傳遞過程中的變量賦值進(jìn)行更深入的探究。通過利用SAT實(shí)例中一個(gè)不滿足的子句至少有一個(gè)變量分類錯(cuò)誤，參與更多不滿足子句的變量更有可能被錯(cuò)誤分類這一特性，設(shè)計(jì)了一個(gè)錯(cuò)誤偏好變量嵌入調(diào)整算法。該算法利用消息傳遞過程中的變量賦值來計(jì)算每個(gè)變量參與未滿足子句的情況，將其中參與未滿足子句的變量稱為錯(cuò)誤偏好變量，并在消息傳遞過程中重點(diǎn)調(diào)整錯(cuò)誤偏好變量的嵌入來得到一組新的變量嵌入。

其次，對于一個(gè)SAT實(shí)例，如果將所有變量的賦值作為監(jiān)督信號，這些信號之間存在復(fù)雜的約束。例如，一個(gè)變量的值可能決定另一個(gè)變量的值，也可能使另一個(gè)變量的取值變得無關(guān)緊要。SAT實(shí)例的這一特點(diǎn)要求算法對監(jiān)督信號進(jìn)行精心設(shè)計(jì)。Cameron等人^［22］使用實(shí)例的一組解作為監(jiān)督信號，由于搜索空間過大，最終模型輸出的一組解難以滿足整個(gè)實(shí)例。NSNet^［23］使用變量在多組解中的均值作為監(jiān)督信號，然而最終模型預(yù)測值為變量取true的概率，不能直接輸出一組可滿足解，且為所有訓(xùn)練集問題實(shí)例尋找多組可滿足解的代價(jià)較高。QuerySAT^［19］設(shè)計(jì)了一個(gè)無監(jiān)督損失函數(shù)來訓(xùn)練模型，能夠直接預(yù)測問題的一組解，但其要求訓(xùn)練集均為可滿足實(shí)例，卻沒有利用到數(shù)據(jù)集中提供的可滿足實(shí)例的一組可行解。本文在該無監(jiān)督損失函數(shù)的基礎(chǔ)上利用SAT問題實(shí)例變量之間存在復(fù)雜依賴關(guān)系這一特性，設(shè)計(jì)了一個(gè)動(dòng)態(tài)部分標(biāo)簽監(jiān)督訓(xùn)練模式。該模式避免為所有變量提供標(biāo)簽，同時(shí)利用到了數(shù)據(jù)集中的一組可滿足解為部分錯(cuò)誤偏好變量提供標(biāo)簽，保持了一個(gè)較小的搜索空間。

總之，本文提出了一個(gè)全新的基于SAT問題實(shí)例特性的端到端SAT求解模型，其名為錯(cuò)誤偏好變量嵌入架構(gòu)AEEV（architecture of embedding error-preference variables）。本文主要貢獻(xiàn)如下：

a）本文提出了錯(cuò)誤偏好變量嵌入調(diào)整算法。該算法通過統(tǒng)計(jì)消息傳遞過程中變量參與未滿足子句的情況來識別錯(cuò)誤偏好變量并調(diào)整其嵌入。

b）本文提出了動(dòng)態(tài)部分標(biāo)簽監(jiān)督訓(xùn)練模式。該模式通過在訓(xùn)練過程中將錯(cuò)誤偏好變量的標(biāo)簽修改為其在一組解中的真實(shí)賦值，并將其他變量的標(biāo)簽保留為預(yù)測值，從而管理更小的搜索空間。

本文將QuerySAT和NeuroSAT與AEEV在四個(gè)隨機(jī)SAT數(shù)據(jù)集（k-SAT、3-SAT、3-Clique和k-Coloring）上進(jìn)行了比較。實(shí)驗(yàn)結(jié)果表明，AEEV在其中三個(gè)任務(wù)上優(yōu)于當(dāng)前先進(jìn)的端到端SAT求解模型QuerySAT，在包含600個(gè)變量的k-SAT數(shù)據(jù)集上準(zhǔn)確率提升了45.81%。

此外，AEEV在SAT競賽數(shù)據(jù)集和隨機(jī)3-SAT數(shù)據(jù)集上超越了兩個(gè)著名的基于CDCL的經(jīng)典求解器：CaDiCaL^［23］和Kissat^［24］。在工業(yè)問題——SHA-1原像攻擊任務(wù)上超越了基于SLS的求解器GSAT。結(jié)果表明，AEEV在多種SAT問題類型求解上展現(xiàn)了良好的泛化性能。

1 SAT問題的表示形式

由于任意一個(gè)布爾表達(dá)式都可以通過Tseitin算法在線性時(shí)間內(nèi)轉(zhuǎn)換為一個(gè)等價(jià)的合取范式CNF（conjunctive normal form）^［25］，本文主要關(guān)注以合取范式表示的SAT實(shí)例。

在一個(gè)合取范式中，SAT實(shí)例?由一系列析取子句{c_i}^m_i=1用合取操作符連接得到，一個(gè)析取子句c_i則由一系列變量x_j對應(yīng)的正文字x_j和負(fù)文字?x_j用析取操作符連接起來。例如在SAT實(shí)例?=（x₁∨x₂）∧（?x₁∨x₂∨?x₃）∧（?x₂∨x₃）中，c₁=（x₁∨x₂）、c₂=（?x₁∨x₂∨?x₃）、c₃=（?x₂∨x₃）是子句，x₁為正文字，?x₁為對應(yīng)的負(fù)文字。

由于CNF范式具有的良好結(jié)構(gòu)，一個(gè)包含n個(gè)變量和m個(gè)子句的CNF范式?又可以轉(zhuǎn)換為一個(gè)對應(yīng)的無向二分圖G（L，C，E）。其中L為所有變量對應(yīng)的正負(fù)文字構(gòu)成的頂點(diǎn)集， |L|=2n；C為所有子句構(gòu)成的頂點(diǎn)集，|C|=m；E為邊集，如果一個(gè)子句包含某個(gè)文字，那么存在該子句節(jié)點(diǎn)到對應(yīng)文字節(jié)點(diǎn)的一條連邊。這種無向二分圖也稱為文字-子句圖，如圖1所示。

通過將問題建模為二分圖表示，SAT求解問題轉(zhuǎn)換為了無向二分圖上的變量節(jié)點(diǎn)二分類問題。

2 錯(cuò)誤偏好變量嵌入架構(gòu)

如圖2所示，模型主要分為重要子句識別模塊、錯(cuò)誤偏好變量嵌入調(diào)整模塊和動(dòng)態(tài)部分標(biāo)簽監(jiān)督模塊三個(gè)模塊。

在重要子句識別模塊，模型將一個(gè)文字-子句圖表示的SAT實(shí)例輸入到一個(gè)消息傳遞網(wǎng)絡(luò)中，消息傳遞網(wǎng)絡(luò)輸出這個(gè)問題的原始變量嵌入V_r， 并且使用分類器O對原始變量嵌入進(jìn)行分類來得到一組原始解S_r， S_r將被用于統(tǒng)計(jì)未被滿足的子句并且識別重要子句，一旦識別出重要子句，原始變量嵌入V_r將被輸入到錯(cuò)誤偏好變量嵌入調(diào)整模塊中進(jìn)行調(diào)整。在錯(cuò)誤偏好變量嵌入調(diào)整模塊，原始變量嵌入V_r和SAT實(shí)例的鄰接矩陣M將被用于計(jì)算出一個(gè)錯(cuò)誤偏好矩陣P，錯(cuò)誤偏好矩陣P和原始變量嵌入V_r點(diǎn)積的結(jié)果將與原始變量嵌入V_r一起輸入到一個(gè)嵌入調(diào)整網(wǎng)絡(luò)R中來計(jì)算得到調(diào)整后的變量嵌入V_n。在動(dòng)態(tài)部分標(biāo)簽監(jiān)督模塊，原始變量嵌入V_r經(jīng)過分類器O分類得到的解S_r將與一組真實(shí)解S_g生成一組部分監(jiān)督標(biāo)簽S_h，同時(shí)，調(diào)整后的變量嵌入V_n經(jīng)過分類器O分類會(huì)得到的一個(gè)新解S_n，部分監(jiān)督標(biāo)簽S_h和新解S_n經(jīng)過部分監(jiān)督損失函數(shù)計(jì)算得到部分監(jiān)督損失，這個(gè)損失值將用于模型訓(xùn)練。

2.1 重要子句識別模塊

重要子句識別模塊主要由一個(gè)預(yù)訓(xùn)練的消息傳遞網(wǎng)絡(luò)和一個(gè)重要子句統(tǒng)計(jì)模塊組成。

消息傳遞網(wǎng)絡(luò)的輸入是一個(gè)三元組G=（M，V，C），在消息傳遞的每一個(gè)輪次輸出一個(gè)問題的原始變量嵌入V_r，如式（1）所示。

V_r=MPNN（M，V，C）（1）

其中：M∈{0，1}^2n×m是文字-子句圖表示的SAT問題的鄰接矩陣，n表示問題的變量數(shù)，m表示問題的子句數(shù)；V∈?^n×d表示變量嵌入矩陣，C∈?^m×d表示子句嵌入矩陣，d表示嵌入的維度。AEEV中消息傳遞網(wǎng)絡(luò)的具體結(jié)構(gòu)來自文獻(xiàn)［21］。

變量嵌入V_r經(jīng)過分類器O分類后得到一組解S_r∈{0，1}ⁿ，如式（2）所示。

S_r=O（V_r）（2）

重要子句統(tǒng)計(jì)模塊將通過S_r計(jì)算得到每一個(gè)子句的滿足情況，并且按照式（3）為每個(gè)子句更新其重要性分?jǐn)?shù)sc∈［0，1］^m。

sc_i=k_iT_n（3）

其中：kc_i∈N^m是在重要性分?jǐn)?shù)統(tǒng)計(jì)期間子句i未被滿足的次數(shù)，T_n∈N₊表示從上一個(gè)統(tǒng)計(jì)期間結(jié)束到當(dāng)前輪次的消息傳遞次數(shù)。

重要性分?jǐn)?shù)sc將被用于計(jì)算一個(gè)布爾值ICs， 如式（4）所示。

ICs=（T_ngt;T_m）∧（max（sc）gt;t）（4）

其中：T_m表示調(diào)整的最小調(diào)整間隔，t是一個(gè)閾值，T_m和t都是超參數(shù)。當(dāng)消息傳遞的輪次達(dá)到最小調(diào)整間隔且至少存在一個(gè)子句的重要性分?jǐn)?shù)大于閾值t時(shí)，當(dāng)前消息傳遞輪次輸出的變量嵌入將被送入錯(cuò)誤偏好變量嵌入調(diào)整模塊進(jìn)行嵌入調(diào)整。

2.2 錯(cuò)誤偏好變量嵌入調(diào)整模塊

錯(cuò)誤偏好變量嵌入調(diào)整模塊將變量嵌入V_r和鄰接矩陣M作為輸入，并且輸出調(diào)整后的變量嵌入V_n∈?^n×d，計(jì)算過程分為三步。

首先通過式（5）計(jì)算得到每一個(gè)子句的嵌入。

C=M^T×（V_r，－V_r）D_c（5）

其中：D_c表示每個(gè)子句的度。

之后，子句嵌入C將會(huì)被用于計(jì)算每一個(gè)文字節(jié)點(diǎn)的消息，如式（6）所示。

L_p，L_n=M×CD_t（6）

其中：L_p表示正文字的嵌入；L_n表示負(fù)文字的嵌入；D_t表示文字節(jié)點(diǎn)的度。

最后，變量的正文字嵌入和負(fù)文字嵌入相加并通過tanh函數(shù)映射到（-1，1），來得到變量的錯(cuò)誤偏好嵌入矩陣P， P將會(huì)與原始變量嵌入V_r點(diǎn)乘，結(jié)果和原始變量嵌入一起輸入調(diào)整網(wǎng)絡(luò)R中，輸出得到新的變量嵌入V_n，如式（7）所示。

P=tanh（L_p+L_n）V_n=R（P⊙V_r，V_r）（7）

在預(yù)測時(shí)，新的變量嵌入將被送回消息傳遞網(wǎng)絡(luò)中進(jìn)行下一輪的迭代，而在訓(xùn)練階段，新變量嵌入將被用于計(jì)算一個(gè)部分監(jiān)督損失來訓(xùn)練網(wǎng)絡(luò)O和R。

2.3 動(dòng)態(tài)部分標(biāo)簽監(jiān)督模塊

生成部分監(jiān)督標(biāo)簽S_h∈{0，1}ⁿ的過程如圖3所示。其中最頂層的紅色方塊表示未滿足的子句，與頂層紅色方塊實(shí)線連接的第二層的方塊表示參與未滿足子句的變量，其中S_g表示SAT問題的一組真實(shí)解，S_r表示修改后的變量嵌入分類得到的解。最后一行表示最終生成的部分監(jiān)督標(biāo)簽，其中虛線表明了標(biāo)簽值的來源。

部分監(jiān)督損失_A的計(jì)算如式（8）所示。

S_n=O（V_n）

其中：α和β為兩個(gè)超參數(shù)。

2.4 訓(xùn)練

AEEV中的分類器O和糾正網(wǎng)絡(luò)R均為包含了兩個(gè)隱層的MLP，MPNN的網(wǎng)絡(luò)參數(shù)設(shè)置和QuerySAT相同。AEEV的訓(xùn)練分為兩個(gè)階段：第一個(gè)階段，訓(xùn)練MPNN消息傳遞網(wǎng)絡(luò)和分類器O；第二個(gè)階段固定MPNN的參數(shù)，訓(xùn)練分類器O和糾正網(wǎng)絡(luò)R。

3 實(shí)驗(yàn)與分析

實(shí)驗(yàn)配置：NVIDIA GeForce GTX 2080 SUPER（8 GB） 顯卡、 Intel? Xeon? CPU E5-2690 v3 @ 2.60 GHz 處理器、64 GB內(nèi)存。使用TensorFlow深度學(xué)習(xí)框架實(shí)現(xiàn)。

3.1 數(shù)據(jù)集

本文選用k-SAT、3-SAT、k-Coloring和3-Clique四個(gè)隨機(jī)SAT問題數(shù)據(jù)集、一個(gè)工業(yè)SAT問題數(shù)據(jù)集SHA-1原像攻擊以及一個(gè)SAT競賽數(shù)據(jù)集作為實(shí)驗(yàn)數(shù)據(jù)集，接下來是對數(shù)據(jù)集的參數(shù)和規(guī)模的介紹。

對于隨機(jī)SAT數(shù)據(jù)集的參數(shù)，本文采用文獻(xiàn)［20］的生成算法和參數(shù)生成k-SAT數(shù)據(jù)集，使用CNFgen^［26］庫生成其他三個(gè)數(shù)據(jù)集。其中，3-SAT問題實(shí)例的子句（m）變量（n）比率設(shè)置為m=4.258n+58.26n^［27］。對于數(shù)據(jù)集中的問題規(guī)模，k-SAT訓(xùn)練集中問題實(shí)例的變量數(shù)為3～100，測試集變量數(shù)3～600；對于3-SAT問題數(shù)據(jù)集，訓(xùn)練集變量數(shù)為5～100，測試集變量數(shù)5～405；對于兩個(gè)圖問題3-Clique和k-Coloring，訓(xùn)練集的圖中頂點(diǎn)數(shù)為4～40，但是測試集中，3-Clique頂點(diǎn)數(shù)為4～200，k-Coloring頂點(diǎn)數(shù)為40～120。以上數(shù)據(jù)集的訓(xùn)練集均包含了10萬個(gè)問題實(shí)例，測試集包含1萬個(gè)問題實(shí)例。

此外，本文還為3-SAT任務(wù)生成了變量數(shù)100～400，間隔為50的固定變量大小的測試集；為k-SAT問題生成了變量數(shù)100～600，間隔為100的測試集；用于測試隨著SAT問題規(guī)模增大，模型準(zhǔn)確率的變化。以上每個(gè)測試集均包含1萬個(gè)問題實(shí)例。

為了評估模型在SAT競賽中的表現(xiàn)，實(shí)驗(yàn)從歷年的SAT競賽中收集了517個(gè)變量數(shù)在250～800的3-SAT問題實(shí)例作為SAT競賽測試集。

為了評估模型在工業(yè)問題數(shù)據(jù)集中的表現(xiàn)，實(shí)驗(yàn)從2019年SAT競賽中選擇了SHA-1原像攻擊任務(wù)^［28］，在該任務(wù)數(shù)據(jù)集上進(jìn)行實(shí)驗(yàn)。SHA-1原像攻擊任務(wù)的目標(biāo)是從給定的hash值中找到對應(yīng)的消息輸入，該任務(wù)可以被轉(zhuǎn)換為一個(gè)SAT問題求解任務(wù)，實(shí)驗(yàn)使用CGen^［29］工具生成了包含10萬個(gè)實(shí)例的訓(xùn)練集以及5 000個(gè)實(shí)例的測試集。

3.2 參數(shù)設(shè)置

在訓(xùn)練時(shí)，AEEV使用AdaBelief^［30］作為優(yōu)化器，學(xué)習(xí)率為0.000 2，節(jié)點(diǎn)嵌入的維度為128，最小迭代次數(shù)T_m設(shè)置為64，閾值t為0.7，損失函數(shù)的兩個(gè)超參數(shù)α和β設(shè)置為1，每個(gè)問題實(shí)例消息傳遞的次數(shù)為32。

在訓(xùn)練的第一個(gè)階段，在隨機(jī)SAT問題數(shù)據(jù)集上訓(xùn)練50萬個(gè)輪次，在SHA-1原像攻擊任務(wù)數(shù)據(jù)集上訓(xùn)練100萬個(gè)輪次。在第二個(gè)階段，所有在所有數(shù)據(jù)集上均訓(xùn)練1萬個(gè)輪次。

3.3 和SOTA模型的準(zhǔn)確率對比

實(shí)驗(yàn)選取了當(dāng)前較先進(jìn)的基于神經(jīng)網(wǎng)絡(luò)的端到端求解模型QuerySAT和基線模型NeuroSAT作為對比模型，由于NeuroSAT不能直接輸出變量的賦值，只能判斷問題的可滿足性，本文對其進(jìn)行了改進(jìn)，添加了一個(gè)分類器O來對NeuroSAT的節(jié)點(diǎn)嵌入進(jìn)行分類。在測試階段，消息傳遞的消息傳遞輪為512。

實(shí)驗(yàn)結(jié)果如表1所示，本文中的準(zhǔn)確率均指模型求解的問題實(shí)例個(gè)數(shù)占總測試集實(shí)例個(gè)數(shù)的比例。所有實(shí)驗(yàn)均進(jìn)行了三次，并計(jì)算準(zhǔn)確率的均值和標(biāo)準(zhǔn)差。和基線模型NeuroSAT相比，在所有的四個(gè)數(shù)據(jù)集上AEEV均超越了NeuroSAT，對于兩個(gè)圖問題數(shù)據(jù)集3-Clique和k-Coloring，NeuroSAT幾乎無法求解而AEEV分別取得了97.77%和98.17%的準(zhǔn)確率。和QuerySAT相比，AEEV在3-SAT數(shù)據(jù)集上準(zhǔn)確率較為接近，只低3.05%，而在k-SAT數(shù)據(jù)集上提升了6.63%。

3.4 AEEV的泛化性能分析

為了進(jìn)一步分析各個(gè)模型在更大規(guī)模問題數(shù)據(jù)集上的泛化能力，本文評估了三個(gè)模型在變量數(shù)分別為100、200、…、600的k-SAT數(shù)據(jù)集上的表現(xiàn)，結(jié)果如圖4所示。

在求解變量數(shù)在100和200的k-SAT實(shí)例時(shí)，AEEV和QuerySAT的準(zhǔn)確率較為接近，隨著問題規(guī)模的擴(kuò)大，三個(gè)模型的準(zhǔn)確率都在下降，然而AEEV下降得更加緩慢。在變量數(shù)300～600的較大規(guī)模的k-SAT問題上，AEEV的優(yōu)勢更加明顯，具體而言，在變量數(shù)為600時(shí)，AEEV的準(zhǔn)確率相較QuerySAT提升了17.6%。

3.5 超參數(shù)設(shè)置對實(shí)驗(yàn)結(jié)果的影響

本節(jié)驗(yàn)證了最小調(diào)整間隔T_m以及測試階段的消息傳遞輪次兩個(gè)主要超參數(shù)對模型準(zhǔn)確率的影響。

圖5顯示了測試階段消息傳遞輪次對模型準(zhǔn)確率的影響，三個(gè)模型均在變量數(shù)為3～100的k-SAT數(shù)據(jù)集上訓(xùn)練，分別在變量數(shù)為3～600的k-SAT測試集上進(jìn)行測試，測試階段模型的消息傳遞次數(shù)分別設(shè)置為64、128、256、…、4 096?？梢园l(fā)現(xiàn)隨著消息傳遞輪次的增加，三個(gè)模型在不同問題規(guī)模數(shù)據(jù)集上的準(zhǔn)確率均得到了提升，但是AEEV有著更快的提升速度。在變量數(shù)為600的較大規(guī)模的k-SAT測試集上，隨著迭代輪次增加，QuerySAT的準(zhǔn)確率趨近基線模型NeuroSAT，在迭代輪次為4 096時(shí)，AEEV求解了56.43%的SAT實(shí)例，而QuerySAT和NeuroSAT只求解了約10%，其中QuerySAT準(zhǔn)確率為10.62%，AEEV相較于QuerySAT提升了45.81%。

最小調(diào)整間隔T_m是AEEV的一個(gè)重要超參數(shù)，決定了錯(cuò)誤變量嵌入糾正模塊至少間隔多少個(gè)消息傳遞輪次對變量嵌入進(jìn)行調(diào)整。圖6顯示了最小調(diào)整間隔T_m對AEEV的影響，其中AEEV模型在變量數(shù)為3～100的k-SAT數(shù)據(jù)集上訓(xùn)練，在變量數(shù)分別為200、400、600的k-SAT測試集上測試，測試階段T_m設(shè)置為8、16、…、512，消息傳遞輪次為2 048。實(shí)驗(yàn)結(jié)果表明，T_m的最優(yōu)值會(huì)隨著問題規(guī)模的變化而變化，當(dāng)在包含200個(gè)變量的k-SAT測試集上，最優(yōu)T_m取值在128附近，隨著問題規(guī)模的增大，最優(yōu)T_m值隨之變小，在變量數(shù)為400的k-SAT測試集上，最優(yōu)T_m值在64附近，在變量數(shù)為600的k-SAT測試集上，最優(yōu)T_m在32附近。

3.6 消融實(shí)驗(yàn)

AEEV由三個(gè)模塊組成，其中重要子句識別模塊僅用于節(jié)點(diǎn)嵌入生成以及判斷是否需要進(jìn)行嵌入糾正，無優(yōu)化策略。為充分驗(yàn)證嵌入糾錯(cuò)模塊和部分監(jiān)督模塊對模型的性能都有提升效果，本文構(gòu)建了AEEV的兩個(gè)變種：AEEV-R和AEEV-DL模型。AEEV-R不包含錯(cuò)誤偏好變量嵌入調(diào)整模塊和動(dòng)態(tài)部分標(biāo)簽監(jiān)督模塊，僅包含消息傳遞網(wǎng)絡(luò)和分類網(wǎng)絡(luò)O；AEEV-DL包含錯(cuò)誤偏好變量嵌入調(diào)整模塊，但是不包含動(dòng)態(tài)部分標(biāo)簽監(jiān)督模塊，僅用文獻(xiàn)［14］的無監(jiān)督損失函數(shù)訓(xùn)練。

AEEV、AEEV-R、AEEV-DL模型均在變量數(shù)5～405的3-SAT數(shù)據(jù)集上訓(xùn)練，在變量數(shù)分別為100、150、…、400的測試集上測試，結(jié)果如表2所示。首先比較AEEV-R和AEEV-DL，可以看到加入了錯(cuò)誤偏好變量嵌入糾正模塊的AEEV-DL在各個(gè)規(guī)模的3-SAT測試集上均超越了AEEV-R，其中在變量數(shù)為400的測試集上，錯(cuò)誤偏好變量嵌入糾正模塊帶來了12.35%的提升。再來比較AEEV-DL和AEEV，可以發(fā)現(xiàn)AEEV在所有的測試集上的準(zhǔn)確率均超越了AEEV-DL，且隨著問題規(guī)模的擴(kuò)大，準(zhǔn)確率提升更明顯，在變量數(shù)為350的測試集上，AEEV取得了5.56百分點(diǎn)的提升，在變量數(shù)為400的測試集上，AEEV取得了9.4百分點(diǎn)的提升，結(jié)果說明了動(dòng)態(tài)部分標(biāo)簽監(jiān)督模塊的有效性。

3.7 和經(jīng)典求解器的性能對比

本文選取了Kissat和CaDiCal兩個(gè)基于CDCL的經(jīng)典求解器，以及一個(gè)基于SLS的經(jīng)典求解器GSAT作為對比算法。在隨機(jī)生成的包含400個(gè)變量的3-SAT數(shù)據(jù)集、SAT競賽數(shù)據(jù)集以及SHA-1原像攻擊任務(wù)數(shù)據(jù)集上進(jìn)行性能對比。Kissat求解器是2020年SAT競賽主賽道的第一名，CaDiCal是2019年SAT競賽主賽道的第一名，GSAT是著名的非完備求解器。對于3-SAT任務(wù)以及SAT競賽任務(wù)，AEEV模型在變量數(shù)為5～405的3-SAT數(shù)據(jù)集上訓(xùn)練，對于SHA-1原像攻擊任務(wù)，AEEV模型在變量數(shù)5～10 000的SHA-1訓(xùn)練集上訓(xùn)練，測試時(shí)消息傳遞次數(shù)均設(shè)置為1 024，最小調(diào)整間隔為64。對于Kissat和CaDiCal求解器，本次實(shí)驗(yàn)為每個(gè)SAT實(shí)例設(shè)置了5 s的超時(shí)時(shí)間，對于GSAT求解器，最大翻轉(zhuǎn)次數(shù)為50萬次。

圖7顯示了AEEV和經(jīng)典求解器在生成的3-SAT數(shù)據(jù)集上的結(jié)果，其中AEEV在25 386 s的時(shí)間里求解了6 319個(gè)實(shí)例，Kissat在25 215 s中求解了5 620個(gè)實(shí)例，CaDiCal用時(shí)35 768 s求解了4 617個(gè)實(shí)例，GSAT在2 271 s中求解了9 216個(gè)實(shí)例。圖8展現(xiàn)了算法在收集的SAT競賽數(shù)據(jù)集上的結(jié)果，其中AEEV在1 694 s里求解了112個(gè)實(shí)例，Kissat在2 258 s中求解了89個(gè)實(shí)例，CaDiCal在2 354 s中求解了69個(gè)實(shí)例，GSAT在448 s中求解了192個(gè)實(shí)例?？梢园l(fā)現(xiàn)，在隨機(jī)SAT任務(wù)上GSAT有較大優(yōu)勢，而AEEV的表現(xiàn)超過了兩個(gè)基于CDCL的求解器。

圖9展現(xiàn)了不同算法在工業(yè)SAT問題數(shù)據(jù)集——SHA-1原像攻擊任務(wù)上的表現(xiàn)?？梢钥吹?，基于CDCL的求解器CaDiCal和Kissat快速完成了對5 000個(gè)問題實(shí)例的求解，GSAT最終求解了1 013個(gè)問題實(shí)例，而AEEV最終求解了1 642個(gè)問題實(shí)例。

從實(shí)驗(yàn)結(jié)果可以發(fā)現(xiàn)，AEEV在隨機(jī)SAT求解任務(wù)上超越了兩個(gè)基于CDCL的求解器，在工業(yè)SAT求解任務(wù)上超越了基于SLS的求解器，在各類SAT問題求解上展現(xiàn)了良好的泛化性能。

4 結(jié)束語

本文基于SAT問題實(shí)例特性提出了一個(gè)端到端SAT求解模型AEEV，該模型主要包含錯(cuò)誤偏好變量嵌入調(diào)整算法和動(dòng)態(tài)部分標(biāo)簽監(jiān)督訓(xùn)練模式。錯(cuò)誤偏好變量嵌入調(diào)整算法利用了SAT問題中參與更多未滿足子句的變量更可能被錯(cuò)誤分類這一特性，在消息傳遞過程中識別錯(cuò)誤偏好變量并修改其嵌入。動(dòng)態(tài)部分標(biāo)簽監(jiān)督訓(xùn)練模式則利用了SAT問題變量之間存在復(fù)雜約束關(guān)系這一特性，在訓(xùn)練過程中為錯(cuò)誤偏好變量提供來自一組真實(shí)值的標(biāo)簽，并保持其他變量的標(biāo)簽為預(yù)測值不變。實(shí)驗(yàn)表明，AEEV在多個(gè)任務(wù)上優(yōu)于目前最先進(jìn)的基于神經(jīng)網(wǎng)絡(luò)的端到端SAT求解模型QuerySAT和改進(jìn)版的SAT求解模型NeuroSAT，在解決較大規(guī)模的SAT實(shí)例時(shí)，AEEV的優(yōu)勢更為明顯。此外，本文將AEEV與多個(gè)經(jīng)典求解器：Kissat、CaDiCal以及GSAT進(jìn)行了比較。結(jié)果表明，AEEV模型在隨機(jī)SAT問題求解任務(wù)上超越了Kissat以及CaDiCal，在工業(yè)SAT問題求解上超越了GSAT，展現(xiàn)了AEEV在各類SAT問題求解上的良好泛化性能。

對于未來工作，最小調(diào)整間隔是實(shí)驗(yàn)中的一個(gè)重要參數(shù)，其最優(yōu)值與問題規(guī)模相關(guān)，且顯著影響模型的準(zhǔn)確率，最優(yōu)最小調(diào)整間隔的自適應(yīng)選擇是今后的研究方向之一。

參考文獻(xiàn)：

［1］COOK S A. The complexity of theorem-proving procedures ［C］// Proc of the 3rd Annual ACM Symposium on Theory of Computing. New York：ACM Press， 1971： 151-158.

［2］Goldberg E I， Prasad M R， Brayton R K. Using sat for combinational equivalence checking ［C］// Proc of Design， Automation and Test in Europe Conference and Exhibition. Piscataway，NJ：IEEE Press， 2001： 114-121.

［3］Kuehlmann A， Paruthi V， Krohm F， et al. Robust boolean reasoning for equivalence checking and functional property verification ［J］. IEEE Trans on Computer-Aided Design of Integrated Circuits and Systems， 2002， 21（12）： 1377-1394.

［4］Vizel Y， Weissenbacher G， Malik S. Boolean satisfiability solvers and their applications in model checking ［J］. Proceedings of the IEEE， 2015， 103（11）： 2021-2035.

［5］Prasad M R， Biere A， Gupta A. A survey of recent advances in sat-based formal verification ［J］. International Journal on Software Tools for Technology Transfer， 2005， 7： 156-173.

［6］Hasan O， Tahar S. Formal verification methods ［M］// Encyclopedia of Information Science and Technology. 3rd ed.［S.l.］： IGI Global， 2015： 7162-7170.

［7］Ivani? F， Yang Zijiang， Ganai M K， et al. Efficient SAT-based bounded model checking for software verification ［J］. Theoretical Computer Science， 2008， 404（3）： 256-274.

［8］Jhala R， Majumdar R. Software model checking ［J］. ACM Computing Surveys， 2009， 41（4）： 1-54.

［9］Mironov I， Zhang Lintao. Applications of sat solvers to cryptanalysis of hash functions ［C］//Proc of the 9th International Conference on Theory and Applications of Satisfiability Testing. Berlin：Springer， 2006： 102-115.

［10］Massacci F， Marraro L. Logical cryptanalysis as a sat problem ［J］. Journal of Automated Reasoning， 2000， 24： 165-203.

［11］趙海軍， 陳華月， 崔夢天. 基于改進(jìn)連續(xù)時(shí)間動(dòng)態(tài)系統(tǒng)的模擬SAT求解器 ［J］. 計(jì)算機(jī)應(yīng)用研究， 2024， 41（1）： 200-205. （Zhao Haijun， Chen Huayue， Cui Mengtian. Analog SAT solver based on improved continuous-time dynamic systems ［J］. Application Research of Computers， 2024， 41（1）： 200-205.）

［12］謝志新， 王曉峰， 曹澤軒， 等. 求解可滿足性問題的信息傳播算法研究綜述 ［J］. 計(jì)算機(jī)應(yīng)用研究， 2022， 39（7）： 1933-1940. （Xie Zhixin， Wang Xiaofeng， Cao Zerui， et al. Overview of message propagation algorithm for satisfiability problems ［J］. Application Research of Computers， 2022， 39（7）： 1933-1940.）

［13］郭瑩， 張長勝， 張斌. 求解SAT問題的算法的研究進(jìn)展 ［J］. 計(jì)算機(jī)科學(xué)， 2016， 43（3）： 8-17. （Guo Ying， Zhang Changsheng， Zhang Bin. Research advance of SAT solving algorithm ［J］. Computer Science， 2016， 43（3）： 8-17.）

［14］張建民， 沈勝宇， 李思昆. 可滿足性求解技術(shù)研究 ［J］. 計(jì)算機(jī)工程與科學(xué)， 2010， 32（1）： 50-54. （Zhang Jianmin， Shen Shengyu， Li Sikun. Advances in satisfiability solving techniques ［J］. Computer Engineering amp; Science， 2010， 32（1）： 50-54.）

［15］Guo Wenxuan，Zhen Huiling，Li Xijun， et al. Machine learning me-thods in solving the boolean satisfiability problem ［J］. Machine Intelligence Research， 2023，20（5）：640-655.

［16］Amizadeh S， Matusevych S， Weimer M. Learning to solve Circuit-SAT： an unsupervised differentiable approach ［C］//Proc of International Conference on Learning Representations. 2018： 1-14.

［17］Li Zhaoyu， Si Xujie. NSNet： a general neural probabilistic framework for satisfiability problems ［C］// Proc of the 36th International Conference on Neural Information Processing Systems. 2024： 25573-25585.

［18］Zhang Chenhao， Zhang Yanjun， Mao J， et al. Towards better gene-ralization for neural network-based sat solvers ［C］// Proc of the 26th Pacific-Asia Conference on Knowledge Discovery and Data Mining. Berlin：Springer， 2022： 199-210.

［19］Kurin V， Godil S， Whiteson S， et al. Improving SAT solver heuristics with graph networks and reinforcement learning ［EB/OL］. （2020）. https：//openreview. net/forum？id=B1lC n64tvS.

［20］Selsam D， Lamm M， Bünz B， et al. Learning a SAT solver from single-bit supervision ［EB/OL］. （2018）.https：//arxiv.org/abs/1802. 03685.

［21］Ozolins E， Freivalds K， Draguns A， et al. Goal-aware neural SAT solver ［C］//Proc of International Joint Conference on Neural Networks. Piscataway，NJ：IEEE Press， 2022： 1-8.

［22］Cameron C， Chen R， Hartford J， et al. Predicting propositional satis-fiability via end-to-end learning ［C］// Proc of AAAI Conference on Artificial Intelligence. Palo Alto， CA： AAAI Press， 2020： 3324-3331.

［23］Queue S D. CaDiCaL at the SAT Race 2019 ［J］. SAT Race， 2019， 2019： 8.

［24］Fleury A， Heisinger M. CADICAL， KISSAT， PARACOOBA， PLINGELING and TREENGELING entering the SAT competition 2020 ［J］. SAT Competition， 2020， 2020： 50.

［25］Tseitin G S. On the complexity of derivation in propositional calculus ［M］// Siekmann J H， Wrightson G. Automation of Reasoning： 2： Classical Papers on Computational Logic. Berlin： Springer， 1983： 466-483.

［26］Lauria M， Elffers J， Nordstr?m J， et al. CNFgen： a generator of crafted benchmarks ［C］//Proc of the 20th International Conference on Theory and Applications of Satisfiability Testing. Berlin：Springer， 2017： 464-473.

［27］Crawford J M， Auton L D. Experimental results on the crossover point in random 3-SAT ［J］. Artificial Intelligence， 1996， 81（1-2）： 31-57.

［28］Skladanivskyy V. Minimalistic round-reduced SHA-1 pre-image attack ［J］. SAT Race， 2019， 2019： 51.

［29］Skladanivskyy V. Tailored compact CNF encoding for SHA-1 ［EB/OL］. （2020）. http：//blog.sophisticatedways.net/2020/10/tailored-compact-cnf-encoding-for-sha-1.html.

［30］Zhuang Juntang， Tang T， Ding Yifan， et al. AdaBelief optimizer： adapting stepsizes by the belief in observed gradients ［C］// Proc of the 34th International Conference on Neural Information Processing Systems. 2020： 18795-18806.