求解布爾SAT的方法

摘要：布爾可滿足性問題（Boolean Satisfiability Problem，簡(jiǎn)稱SAT問題）是邏輯學(xué)和計(jì)算機(jī)科學(xué)中的一個(gè)問題，它的目的是確定是否存在一種解釋，使給定的布爾公式成立。換句話說，它詢問給定布爾公式的變量是否可以被一致地替換為真值或假值，使公式求值為真。如果是這樣，那么這個(gè)公式就是可滿足的。另一方面，如果不存在這樣的賦值，那么該公式所表示的函數(shù)對(duì)于所有可能的變量賦值都為假，該公式不可滿足1。

追根溯源，SAT是第一個(gè)已知的NP-Complete問題，多倫多大學(xué)的Stephen Cook在1971年，國(guó)家科學(xué)院的Leonid Levin在1973年均獨(dú)立證明了這一問題。在此之前，NP-Complete問題的概念甚至不存在。另外，證明顯示復(fù)雜性類NP中的每個(gè)決策問題都可以簡(jiǎn)化為CNF公式的SAT問題，有時(shí)也稱為“CNFSAT”。

值得注意的是，SAT問題是計(jì)算機(jī)科學(xué)領(lǐng)域最基本的問題之一，有著重要的理論意義和實(shí)際應(yīng)用。在理論研究中，SAT問題是一個(gè)經(jīng)典的判定問題，同樣是第一個(gè)被證明為NP-Complete的問題。這個(gè)決策問題在包括理論計(jì)算機(jī)科學(xué)、復(fù)雜性理論、算法、密碼學(xué)和人工智能等計(jì)算機(jī)科學(xué)的各個(gè)領(lǐng)域都至關(guān)重要。

在現(xiàn)實(shí)場(chǎng)景應(yīng)用中，SAT是很多工業(yè)場(chǎng)景里面的核心工具。尤其在一些包括芯片測(cè)試、電路等價(jià)性驗(yàn)證、電路模型檢測(cè)、智慧園區(qū)及無線設(shè)備的布局、操作系統(tǒng)、航空等對(duì)精確度要求很高的核心領(lǐng)域，都需要SAT求解器的重磅參與。例如，芯片SAT分析是一種系統(tǒng)級(jí)應(yīng)用測(cè)試分析方法，通過對(duì)芯片的性能和可靠性進(jìn)行全面的測(cè)試和分析，以評(píng)估芯片在實(shí)際應(yīng)用中的表現(xiàn)。 另外，在騰訊地圖中的語(yǔ)音序列調(diào)度中，采用SAT算法中的約束加權(quán)方法，播報(bào)失敗率從6.20%可降至2.85%，降幅54%，同時(shí)把地圖路網(wǎng)更新的內(nèi)存消耗量降低一半，更新周期縮短一半。

5月，北京玻色量子科技有限公司（以下簡(jiǎn)稱“玻色量子”）在新品發(fā)布會(huì)上推出的100量子比特相干光量子計(jì)算機(jī)真機(jī)——“天工量子大腦”，旨在快速、且高效地求解NP難的組合優(yōu)化問題，尤其是Ising問題。而布爾可滿足性(SAT)和最大可滿足性(Max-SAT)是NP-Complete問題和NP難問題的一類，兩者同等重要且更切合實(shí)際的組合優(yōu)化問題。

目前，求解布爾SAT的方法有很多，比如量子退火和經(jīng)典的隨機(jī)局部搜索(SLS)求解器。然而，它們都需要巨量步驟來解決困難的SAT問題，這將耗費(fèi)大量的時(shí)間和精力。隨著量子計(jì)算技術(shù)的發(fā)展，一個(gè)SAT問題可以轉(zhuǎn)化為一個(gè)Ising/QUBO問題，從而可由玻色量子的“天工量子大腦”快速高效地求出全局最優(yōu)解。

那么，為了更清楚的理解SAT問題，下面首先介紹一些基本術(shù)語(yǔ)。

基本定義和術(shù)語(yǔ)

SAT問題，簡(jiǎn)單地說就是確定是否存在滿足給定布爾公式解釋的問題，它需要判斷給定布爾公式的變量是否可以一致地替換為值TRUE或FALSE，以使公式的計(jì)算結(jié)果為TRUE。如果是這種情況，則公式稱為“滿足”。否則，若不存在這樣的賦值，則公式表示的函數(shù)對(duì)于所有可能的變量賦值都是FALSE，并且公式是不滿足的。例如，公式“a AND NOT b”是可以滿足的，因?yàn)榭梢哉业街礱 = TRUE和b = FALSE，這使得（aANDNOT b）= TRUE。相反，“a AND NOT a”是無法被滿足的，因?yàn)檎也坏竭@樣的a的值。

命題邏輯公式，也稱為布爾表達(dá)式，由變量，運(yùn)算符AND（連接，也用∧表示）、OR（分離，∨）、NOT（否定，?）和括號(hào)構(gòu)成。如果通過為其變量分配適當(dāng)?shù)倪壿嬛担碩RUE，F(xiàn)ALSE）可以使公式為TRUE，則稱該公式是可滿足的。給定公式，布爾可滿足性問題（SAT）是檢查它是否可滿足。

布爾可滿足性問題有幾種特殊情況，其中公式需要具有特定結(jié)構(gòu)。文字是一個(gè)變量，稱為正文字，或變量的否定，稱為負(fù)文字。子句是文字（或單個(gè)文字）的分離。如果一個(gè)子句最多包含一個(gè)正文字，則該子句稱為Horn子句。如果公式是條款（或單個(gè)子句）的連接，則公式為合取范式（CNF）。

例如，x1是正文字，?x2是負(fù)文字，x1∨?x2是子句，（x1∨?x2）∧（?x1∨x2∨x3）∧x1是聯(lián)合范式的公式；它的第一和第三個(gè)條款是Horn條款，但它的第二個(gè)條款不是。

最大可滿足性問題（Max-SAT）是確定給定布爾公式（以合取范式表示）中最多有多少個(gè)子句可以通過對(duì)公式變量賦真值來使其成立。它是布爾可滿足性問題的推廣，后者詢問是否存在一種真值賦值使所有子句都成立。

問題描述

2-SAT和3-SAT問題是SAT問題的兩種形式，它們的區(qū)別在于每個(gè)子句中包含的變量數(shù)量不同。

具體來說，2-SAT問題中每個(gè)子句最多包含兩個(gè)變量，形如(a∨b)、（?a∨c）等，其中∨表示邏輯或，?表示邏輯非。而3-SAT問題中每個(gè)子句最多包含三個(gè)變量，形如(a∨?b∨c)、(?a∨b∨?c)等。

因?yàn)?-SAT問題中每個(gè)子句最多包含兩個(gè)變量，所以可以使用一些特殊的算法（如Kosaraju算法和Tarjan算法）在多項(xiàng)式時(shí)間內(nèi)求解。而3-SAT問題則是NP-Complete問題，目前還沒有已知的多項(xiàng)式時(shí)間算法可以解決。由于二元變量存在（0/1或者-1/+1）表達(dá)形式的區(qū)別，常見模型有兩種建模思路，在這里分別進(jìn)行說明。

建模思路一

我們以Max 2-SAT問題進(jìn)行討論，將文字表示為0/1的變量，建立QUBO模型。每個(gè)子句由兩個(gè)文字組成，如果其中一個(gè)或兩個(gè)文字都為真，則滿足一個(gè)子句。對(duì)于這個(gè)問題有三種可能的子句類型，每一種都有一個(gè)傳統(tǒng)的約束，如果子句是真的，則必須滿足。

下面是三種常見的轉(zhuǎn)換情況：

① 無負(fù)文字

例如：(xi∨xj)

傳統(tǒng)約束：(xi+xj)≥1

QUBO懲罰項(xiàng)：(1-xi-xj+xixj)

② 一個(gè)負(fù)文字

例如：（xi∨?xj）

傳統(tǒng)約束：xi+?xj≥1

QUBO懲罰項(xiàng)：（xj-xixj)

③兩個(gè)負(fù)文字

例如：（?xi∨?xj）

傳統(tǒng)約束：?xi+?xj≥1

QUBO懲罰項(xiàng)：（xixj）

注：由于變量xj為1/0，所以?xj=1-xj

對(duì)于每個(gè)子句類型，如果滿足傳統(tǒng)約束，則對(duì)應(yīng)的懲罰等于0；如果不滿足傳統(tǒng)約束，則二次懲罰等于1。給定這種一一對(duì)應(yīng)的關(guān)系，我們可以通過等價(jià)地最小化不滿足的子句數(shù)量來逼近子句數(shù)量最大化問題。通過這種形式我們可以構(gòu)建一個(gè)QUBO模型。

所以，對(duì)于給定的Max 2-SAT算例，我們可以添加與問題子句相關(guān)的二次懲罰項(xiàng)，得到一個(gè)我們想要最小化的復(fù)合懲罰函數(shù)。由于懲罰項(xiàng)均為二次型，因此該懲罰函數(shù)采用QUBO模型形式，min y=xTQx。如果在最小化QUBO模型時(shí)等于零，這意味著我們有一個(gè)滿足所有子句的解；如果等于5，這意味著我們有一個(gè)滿足除5以外的所有子句的解。

我們用以下4個(gè)變量和12個(gè)子句的例子來說明這個(gè)算例的建模和求解過程。

將懲罰項(xiàng)加在一起給出了我們的QUBO模型表達(dá)式：

min y=3+x1-2x4-x2x3+x2x4+2x3x4 (1)

或QUBO模型的矩陣形式：

miny=3+xTQx (2)

則Q矩陣表達(dá)為

求解這個(gè)QUBO模型可以得到y(tǒng)=3-2=1，其中x1=x2=x3=0，x4=1。意思是除一個(gè)子句外的所有子句都滿足。

注：上述QUBO方法已在Kochenberger等人的研究中得到成功應(yīng)用[2]，研究解決了含有數(shù)百個(gè)變量和數(shù)千個(gè)子句的Max 2-SAT問題。這種方法求解Max 2-SAT問題的一個(gè)有趣的特點(diǎn)是，得到的待求解QUBO模型的大小與問題中的子句數(shù)無關(guān)，僅由變量的個(gè)數(shù)決定。因此，一個(gè)含有200個(gè)變量和30000個(gè)子句的Max2-SAT問題可以建模為一個(gè)只含有200個(gè)變量的QUBO模型并求解。

建模思路二

為了更好地理解這個(gè)問題，我們將文字表示為-1/1的變量，繼續(xù)討論一個(gè)3-Sat問題。

我們討論一個(gè)3-Sat子句：

x1∨x2∨x3

該子句通過引入-1/1輔助變量可以映射成二次函數(shù)：

在x0，x1，x2的任意取值中，都有一個(gè)使得K最小的值a。如果我們假設(shè)a總是被設(shè)置為這個(gè)最優(yōu)值，那么除了x0=x1=x2=-1時(shí)能量為+1外，其他取值的最低能量都是-7。下表總結(jié)了有關(guān)變量的取值，其中加粗的數(shù)字是給定x0，x1，x2變量的最低可能能量。

使用這種方法，如果xi在子句中被否定，我們可以通過將xi替換為-xi來編碼任意3-Sat子句?，F(xiàn)在，如果我們對(duì)求和這些每個(gè)子句對(duì)應(yīng)的二次函數(shù)，我們可以得到一個(gè)關(guān)于Nxi自旋變量和Maj輔助自旋的二次函數(shù)，從而得到一個(gè)大小為N+M的Ising/QUBO問題。如果該問題是可滿足的，那么最小的Ising能量將是-7M，如果該問題是不可滿足的問題，那么最小的Ising能量為-7Msat，其中Msat是可滿足子句的個(gè)數(shù)。

問題拓展

MAX-SAT是最大可滿足性問題，是SAT問題的推廣。它要求最大數(shù)量的條款，任何轉(zhuǎn)讓都可以滿足。它具有有效的近似算法，但是NP時(shí)間難以精確解決。

在量子計(jì)算領(lǐng)域，2023年6月，NTT最新的研究提出了一種相干SAT求解器(CSS)的新技術(shù)。使用圖形處理器(GPU)實(shí)現(xiàn)的Cyber-CSS與現(xiàn)有的SLS求解器(如probSAT)相比有一定的競(jìng)爭(zhēng)力。未來通過量子計(jì)算實(shí)現(xiàn)SAT問題的快速求解將成為一種新的有效方法。

如今，玻色量子已基于自研的相干光量子計(jì)算機(jī)真機(jī)——“天工量子大腦”在SAT問題求解上具有顯著的算力優(yōu)勢(shì)，代表了其在NP-Complete問題上的實(shí)用性，以進(jìn)一步拓展更多可實(shí)用化量子計(jì)算應(yīng)用場(chǎng)景。

玻色量子還將啟動(dòng)“燎原計(jì)劃”開發(fā)者平臺(tái)，并持續(xù)對(duì)外開放“天工量子大腦”的真機(jī)測(cè)試，熱忱歡迎更多不同領(lǐng)域的研究伙伴前來了解相干量子計(jì)算的原理和能力，在此基礎(chǔ)上展開共同研發(fā)，用量子計(jì)算去解決更多真實(shí)場(chǎng)景中的問題，讓量子計(jì)算的超強(qiáng)算力能真正服務(wù)于各行各業(yè)，滿足未來時(shí)代對(duì)于計(jì)算的需求。