?
摘要：布爾可滿足性問題（Boolean Satisfiability Problem，簡稱SAT問題）是邏輯學和計算機科學中的一個問題，它的目的是確定是否存在一種解釋，使給定的布爾公式成立。換句話說，它詢問給定布爾公式的變量是否可以被一致地替換為真值或假值，使公式求值為真。如果是這樣，那么這個公式就是可滿足的。另一方面，如果不存在這樣的賦值，那么該公式所表示的函數對于所有可能的變量賦值都為假，該公式不可滿足1。
追根溯源，SAT是第一個已知的NP-Complete問題，多倫多大學的Stephen Cook在1971年，國家科學院的Leonid Levin在1973年均獨立證明了這一問題。在此之前，NP-Complete問題的概念甚至不存在。另外，證明顯示復雜性類NP中的每個決策問題都可以簡化為CNF公式的SAT問題，有時也稱為“CNFSAT”。
值得注意的是，SAT問題是計算機科學領域最基本的問題之一，有著重要的理論意義和實際應用。在理論研究中，SAT問題是一個經典的判定問題，同樣是第一個被證明為NP-Complete的問題。這個決策問題在包括理論計算機科學、復雜性理論、算法、密碼學和人工智能等計算機科學的各個領域都至關重要。
在現實場景應用中，SAT是很多工業場景里面的核心工具。尤其在一些包括芯片測試、電路等價性驗證、電路模型檢測、智慧園區及無線設備的布局、操作系統、航空等對精確度要求很高的核心領域，都需要SAT求解器的重磅參與。例如，芯片SAT分析是一種系統級應用測試分析方法，通過對芯片的性能和可靠性進行全面的測試和分析，以評估芯片在實際應用中的表現。
另外，在騰訊地圖中的語音序列調度中，采用SAT算法中的約束加權方法，播報失敗率從6.20%可降至2.85%，降幅54%，同時把地圖路網更新的內存消耗量降低一半，更新周期縮短一半。
5月16日，北京玻色量子科技有限公司（以下簡稱“玻色量子”）在新品發布會上推出的100量子比特相干光量子計算機真機——“天工量子大腦”，旨在快速、且高效地求解NP難的組合優化問題，尤其是Ising問題🔗。而布爾可滿足性(SAT)和最大可滿足性(Max-SAT)是NP-Complete問題和NP難問題的一類，兩者同等重要且更切合實際的組合優化問題。
目前，求解布爾SAT的方法有很多，比如量子退火和經典的隨機局部搜索(SLS)求解器。然而，它們都需要巨量步驟來解決困難的SAT問題，這將耗費大量的時間和精力。隨著量子計算技術的發展，一個SAT問題可以轉化為一個Ising/QUBO問題，從而可由玻色量子的“天工量子大腦”快速高效地求出全局最優解。
那么，為了更清楚的理解SAT問題，下面首先介紹一些基本術語。
基本定義和術語
SAT問題，簡單地說就是確定是否存在滿足給定布爾公式解釋的問題，它需要判斷給定布爾公式的變量是否可以一致地替換為值?TRUE?或?FALSE，以使公式的計算結果為?TRUE。如果是這種情況，則公式稱為“滿足”。否則，若不存在這樣的賦值，則公式表示的函數對于所有可能的變量賦值都是?FALSE，并且公式是不滿足的。例如，公式“a AND NOT b”是可以滿足的，因為可以找到值a = TRUE和b = FALSE，這使得（a?AND?NOT b）= TRUE。相反，“a AND NOT a”是無法被滿足的，因為找不到這樣的a的值。
命題邏輯公式，也稱為布爾表達式，由變量，運算符AND（連接，也用∧表示）、OR（分離，∨）、NOT（否定，?）和括號構成。如果通過為其變量分配適當的邏輯值（即TRUE，FALSE）可以使公式為TRUE，則稱該公式是可滿足的。給定公式，布爾可滿足性問題（SAT）是檢查它是否可滿足。
布爾可滿足性問題有幾種特殊情況，其中公式需要具有特定結構。文字是一個變量，稱為正文字，或變量的否定，稱為負文字。子句是文字（或單個文字）的分離。如果一個子句最多包含一個正文字，則該子句稱為Horn子句。如果公式是條款（或單個子句）的連接，則公式為合取范式（CNF）。
例如，x1是正文字，?x2是負文字，x1∨?x2是子句，（x1∨?x2）∧（?x1∨x2∨x3）∧x1是聯合范式的公式；它的第一和第三個條款是Horn條款，但它的第二個條款不是。
最大可滿足性問題（Max-SAT）是確定給定布爾公式（以合取范式表示）中最多有多少個子句可以通過對公式變量賦真值來使其成立。它是布爾可滿足性問題的推廣，后者詢問是否存在一種真值賦值使所有子句都成立。
問題描述
2-SAT和3-SAT問題是SAT問題的兩種形式，它們的區別在于每個子句中包含的變量數量不同。
具體來說，2-SAT問題中每個子句最多包含兩個變量，形如(a∨b)、（?a∨c）等，其中∨表示邏輯或，?表示邏輯非。而3-SAT問題中每個子句最多包含三個變量，形如(a∨?b∨c)、(?a∨b∨?c)等。
因為2-SAT問題中每個子句最多包含兩個變量，所以可以使用一些特殊的算法（如Kosaraju算法和Tarjan算法）在多項式時間內求解。而3-SAT問題則是NP-Complete問題，目前還沒有已知的多項式時間算法可以解決。由于二元變量存在（0/1或者-1/+1）表達形式的區別，常見模型有兩種建模思路，在這里分別進行說明。
建模思路一
我們以Max 2-SAT問題進行討論，將文字表示為0/1的變量，建立QUBO模型。每個子句由兩個文字組成，如果其中一個或兩個文字都為真，則滿足一個子句。對于這個問題有三種可能的子句類型，每一種都有一個傳統的約束，如果子句是真的，則必須滿足。
下面是三種常見的轉換情況：
① 無負文字
例如：(xi∨xj)
傳統約束：(xi+xj)≥1
QUBO懲罰項：(1-xi-xj+xixj)
② 一個負文字
例如：（xi∨?xj）
傳統約束：xi+?xj≥1
QUBO懲罰項：（xj-xixj)
③?兩個負文字
例如：（?xi∨?xj）
傳統約束：?xi+?xj≥1
QUBO懲罰項：（xixj）
注：由于變量xj為1/0，所以?xj=1-xj
對于每個子句類型，如果滿足傳統約束，則對應的懲罰等于0；如果不滿足傳統約束，則二次懲罰等于1。給定這種一一對應的關系，我們可以通過等價地最小化不滿足的子句數量來逼近子句數量最大化問題。通過這種形式我們可以構建一個QUBO模型。
所以，對于給定的Max 2-SAT算例，我們可以添加與問題子句相關的二次懲罰項，得到一個我們想要最小化的復合懲罰函數。由于懲罰項均為二次型，因此該懲罰函數采用QUBO模型形式，min y=xTQx。如果在最小化QUBO模型時等于零，這意味著我們有一個滿足所有子句的解；如果等于5，這意味著我們有一個滿足除5以外的所有子句的解。
我們用以下4個變量和12個子句的例子來說明這個算例的建模和求解過程。
將懲罰項加在一起給出了我們的QUBO模型表達式：
min y=3+x1-2x4-x2x3+x2x4+2x3x4? ? ? (1)?? ? ??
或QUBO模型的矩陣形式：
? ? ? ? ? ? min?y=3+xTQx? ? ? ??? ? ? ??(2)
則Q矩陣表達為
求解這個QUBO模型可以得到y=3-2=1，其中x1=x2=x3=0，x4=1。意思是除一個子句外的所有子句都滿足。
注：上述QUBO方法已在Kochenberger等人的研究中得到成功應用[2]，研究解決了含有數百個變量和數千個子句的Max 2-SAT問題。這種方法求解Max 2-SAT問題的一個有趣的特點是，得到的待求解QUBO模型的大小與問題中的子句數無關，僅由變量的個數決定。因此，一個含有200個變量和30000個子句的Max?2-SAT問題可以建模為一個只含有200個變量的QUBO模型并求解。
建模思路二
為了更好地理解這個問題，我們將文字表示為-1/1的變量，繼續討論一個3-Sat問題。
我們討論一個3-Sat子句：
x1∨x2∨x3
該子句通過引入-1/1輔助變量可以映射成二次函數：
在x0，x1，x2的任意取值中，都有一個使得K最小的值a。如果我們假設a總是被設置為這個最優值，那么除了x0=x1=x2=-1時能量為+1外，其他取值的最低能量都是-7。下表總結了有關變量的取值，其中加粗的數字是給定x0，x1，x2變量的最低可能能量。
使用這種方法，如果xi在子句中被否定，我們可以通過將xi替換為-xi來編碼任意3-Sat子句。現在，如果我們對求和這些每個子句對應的二次函數，我們可以得到一個關于Nxi自旋變量和Maj輔助自旋的二次函數，從而得到一個大小為N+M的Ising/QUBO問題。如果該問題是可滿足的，那么最小的Ising能量將是-7M，如果該問題是不可滿足的問題，那么最小的Ising能量為-7Msat，其中Msat是可滿足子句的個數。
問題拓展
MAX-SAT是最大可滿足性問題，是SAT問題的推廣。它要求最大數量的條款，任何轉讓都可以滿足。它具有有效的近似算法，但是NP時間難以精確解決。
在量子計算領域，2023年6月，NTT最新的研究提出了一種相干SAT求解器(CSS)的新技術。使用圖形處理器(GPU)實現的Cyber-CSS與現有的SLS求解器(如probSAT)相比有一定的競爭力。未來通過量子計算實現SAT問題的快速求解將成為一種新的有效方法。
如今，玻色量子已基于自研的相干光量子計算機真機——“天工量子大腦”在SAT問題求解上具有顯著的算力優勢，代表了其在NP-Complete問題上的實用性，以進一步拓展更多可實用化量子計算應用場景。
玻色量子還將啟動“燎原計劃”開發者平臺，并持續對外開放“天工量子大腦”的真機測試，熱忱歡迎更多不同領域的研究伙伴前來了解相干量子計算的原理和能力，在此基礎上展開共同研發，用量子計算去解決更多真實場景中的問題，讓量子計算的超強算力能真正服務于各行各業，滿足未來時代對于計算的需求。
[參考文獻]
[1] Glover, Fred, Kochenberger, Gary, Du, Yu. Quantum Bridge Analytics I: a tutorial on formulating and using QUBO models[J]. 4OR: Quarterly Journal of the Belgian, French and Italian Operations Research Societies,2019,17(4):335-371. DOI:10.1007/s10288-019-00424-y.
[2] Kochenberger G , Glover F , Alidaee B ,et al.Using the unconstrained quadratic program to model and solve Max 2-SAT problems[J].International Journal of Operational Research, 2005, 1(1/2):89--100.DOI:10.1504/IJOR.2005.007435.
[3]?Reifenstein S, Leleu T, McKenna T, et al. Coherent SAT solvers: a tutorial[J]. Advances in Optics and Photonics, 2023, 15(2): 385-441.
[4] 百度百科
https://baike.baidu.com/item/%E5%B8%83%E5%B0%94%E5%8F%AF%E6%BB%A1%E8%B6%B3%E6%80%A7%E9%97%AE%E9%A2%98/4715567?fr=aladdin
)
)
