[發明專利]一種基于可編程邏輯的硬件SAT求解器

有效

• 申請號: 201911416673.4
• 申請日: 2019-12-31
• 公開（公告）號: CN111159631B
• 公開（公告）日: 2023-08-11
• 發明（設計）人: 肖立權;馬柯帆;張建民;賴明澈;徐金波;黎淵;熊澤宇;歐洋;龐征斌;劉路;呂方旭
• 申請（專利權）人: 中國人民解放軍國防科技大學
• 主分類號: G06F17/10
• 分類號: G06F17/10
• 代理公司: 北京豐浩知識產權代理事務所(普通合伙) 11781
• 代理人: 李學康

本發明提供了一種基于可編程邏輯的硬件SAT求解器，包括預處理模塊和FPGA模塊。本發明利用可編程邏輯建立硬件SAT求解器，通過對變元的初始指派進行預處理，提前指導最優真值指派的搜索趨勢，以及求解時優先通過查找預存的概率映射表對應的概率對變元進行翻轉，既解決了現有軟件SAT求解器算法復雜，效率較低，且求解成功率不高的技術問題，又能夠減少額外的時間開銷，進而加快求解器求解的進程，能夠更加高效、便捷地求解相對較大規模的SAT問題。

技術領域

本發明屬于計算機技術領域，具體涉及一種SAT求解器，尤其涉及一種基于可編程邏輯的硬件SAT求解器。

背景技術

SAT問題中(satisifiability?problem，布爾可滿足性問題)，給定一組有限變元集合X＝{x₁,x₂,…,x_n}，x_n可以被賦值為真(1)或假(0)，文字l_i是變元x_i或其否定且有子句C由文字析取(表示“或”的意思)而成，合取范式CNF(conjectured?normalformula)公式由多個子句合取而成，如即是一個有5個變元和4個子句組成的CNF公式。子句中任意文字被賦值為真，則子句為真，或被滿足；子句中所有文字同時賦值為假，則稱指定賦值使得子句為假，或指定賦值使得子句不被滿足，公式為可滿足當且僅當所有子句同時被滿足。SAT問題是指尋找X上所有變元的一組賦值X′:X→{0,1}，使得為真。如果存在這樣的賦值，則是可滿足的；如果不存在這樣的賦值，則是不可滿足的。

SAT問題被史蒂文·庫克(Steven?Cook)于1971年證明為NP完全問題，這意味著可以在多項式時間內非常快速地求解，并且在多項式時間內，NP類的所有其他問題都可歸結為SAT問題。求解SAT問題最直接、粗暴的辦法是枚舉法，即嘗試輸入變元的所有可能賦值，然而，這種算法的求解時間會隨著變元數量的增加呈指數增長。

在過去的幾十年里，解決SAT問題的算法，也稱為SAT求解器，取得了巨大的進步。十多年前認為無法求解的問題，現在可以用先進的SAT求解器在幾秒鐘內得以解決。現代SAT求解器可以集成更為先進的求解技術，通過這些技術開發的軟件求解器甚至能夠解決多大數百萬個變元的難的SAT問題。

當SAT求解器試圖解決一個問題時，它會對變元進行完全或部分賦初值(分別用α和β表示)。對公式完全賦值是對公式中的每一個變元賦0或者1，如α＝(x₁＝1,x₂＝0,x₃＝1,x₄＝1,x₅＝1)。相反，部分賦值是對公式變元集合的子集賦值，如β＝(x₁＝1,x₂＝0)。對公式的賦值應遵循布爾邏輯的規則。例如，子句中存在某個或多個文字為真(即值為1)，則該子句是可滿足的，并可從公式中刪除。如果公式是空的(即不再有需要滿足的子句)，則該公式滿足。相反，如果子句中文字為假，則可從子句中刪除該文字。因此，如果子句是空的，那么該子句就不能被滿足，故簡化后的公式也是不可滿足的。

傳統的SAT求解器都是軟件實現的，其求解算法分為完全算法和不完全算法，完全算法窮盡搜索SAT公式的解空間，理論上一定可以得出某個SAT公式的滿足性結論，但是SAT問題屬于NP問題，其解空間隨著公式的變量個數呈指數增長，所以此種算法效率較低，不適用于求解大規模的SAT問題。不完全算法并不搜索整個解空間，而是采用種種辦法搜索部分解空間，其求解速度較快，但是并不能保證一定能判斷SAT問題的可滿足性。隨著實際SAT問題規模的急劇增大，軟件求解器已經不能快速有效地判定SAT問題的可滿足性。

發明內容

本發明要解決的技術問題是針對背景技術中所涉及到的缺陷，提供一種基于可編程邏輯的硬件SAT求解器，用以解決現有技術中軟件SAT求解器算法復雜，效率較低，且求解成功率不高的技術問題。

為解決上述技術問題，本發明采用以下技術方案：