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

關(guān)鍵詞：布爾可滿足性問題；消息傳遞網(wǎng)絡；機器學習

中圖分類號：TP399 文獻標志碼：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 引言

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

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

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

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

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

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

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

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

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

1 SAT問題的表示形式

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

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

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

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

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

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

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

2.1 重要子句識別模塊

重要子句識別模塊主要由一個預訓練的消息傳遞網(wǎng)絡和一個重要子句統(tǒng)計模塊組成。

消息傳遞網(wǎng)絡的輸入是一個三元組G=（M，V，C），在消息傳遞的每一個輪次輸出一個問題的原始變量嵌入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)絡的具體結(jié)構(gòu)來自文獻［21］。

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

S_r=O（V_r）（2）

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

sc_i=k_iT_n（3）

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

重要性分數(shù)sc將被用于計算一個布爾值ICs， 如式（4）所示。

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

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

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

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

首先通過式（5）計算得到每一個子句的嵌入。

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

其中：D_c表示每個子句的度。

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

L_p，L_n=M×CD_t（6）

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

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

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

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

2.3 動態(tài)部分標簽監(jiān)督模塊

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

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

S_n=O（V_n）

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

2.4 訓練

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

3 實驗與分析

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

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

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

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

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

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

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

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

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

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

3.3 和SOTA模型的準確率對比

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

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

3.4 AEEV的泛化性能分析

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

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

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

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

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

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

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

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

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

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

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

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

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

4 結(jié)束語

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

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

參考文獻：

［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］趙海軍， 陳華月， 崔夢天. 基于改進連續(xù)時間動態(tài)系統(tǒng)的模擬SAT求解器 ［J］. 計算機應用研究， 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］. 計算機應用研究， 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］. 計算機科學， 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］. 計算機工程與科學， 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.