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

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

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

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

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

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

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

基本定義和術(shù)語

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

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

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

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

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

問題描述

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

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

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

建模思路一

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

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

① 無負(fù)文字

例如：(xi∨xj)

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

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

② 一個負(fù)文字

例如：（xi∨?xj）

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

QUBO懲罰項：（xj-xixj)

③兩個負(fù)文字

例如：（?xi∨?xj）

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

QUBO懲罰項：（xixj）

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

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

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

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

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

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

或QUBO模型的矩陣形式：

miny=3+xTQx (2)

則Q矩陣表達(dá)為

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

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

建模思路二

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

我們討論一個3-Sat子句：

x1∨x2∨x3

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

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

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

問題拓展

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

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

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

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