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

有效

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

1.一種基于可編程邏輯的硬件SAT求解器，其特征在于，所述硬件SAT求解器包括：預處理模塊和FPGA模塊；

其中，所述預處理模塊，用于產生CNF公式各變元的初始指派、當前指派下的不可滿足子句以及所述CNF公式的子句和變元信息，并發送給所述FPGA模塊；

其中，所述預處理模塊包括：全文字判斷模塊、正文字賦值模塊、負文字賦值模塊和概率賦值模塊；

所述產生CNF公式各變元的初始指派，具體包括：

所述全文字判斷模塊判斷各變元在CNF公式中是否以全是正文字或全是負文字的形式出現；

所述正文字賦值模塊將在CNF公式中以全是正文字的形式出現的變元初始賦值為1；

所述負文字賦值模塊將在CNF公式中以全是負文字的形式出現的變元初始賦值為0；

所述概率賦值模塊對在CNF公式中不以全是正文字或全是負文字的形式出現的變元按照該變元取值為真的概率產生初始指派；

所述FPGA模塊，用于接收預處理模塊發送的CNF公式各變元的初始指派以及不可滿足子句，并在指定次數內根據預存的概率分布數據翻轉變元，判斷CNF公式是否可滿足；

所述FPGA模塊包括第一存儲模塊；

所述接收預處理模塊發送的CNF公式的子句和變元信息，具體包括：

FPGA模塊將接收到的所述預處理模塊發送的CNF公式的子句和變元信息存儲在所述第一存儲模塊；

所述FPGA模塊還包括第一評估模塊、第二存儲模塊、計數器模塊、變元翻轉模塊、概率映射表、FIFO樹和第二評估模塊；

其中，所述第一評估模塊，用于存儲各變元的初始指派以及計算第一存儲模塊中存儲的子句是否滿足，并將不滿足子句存儲在所述第二存儲模塊；

所述計數器模塊，用于計算所述第二存儲模塊中各個變元翻轉后的break-value值，并將break-value排序；

所述概率映射表，用于預先存儲不同翻轉概率對應的break-value值；

所述變元翻轉模塊，用于將子句變元進行翻轉；

所述FIFO樹，用于存儲經變元翻轉模塊翻轉變元后的子句；

所述第二評估模塊，用于從FIFO樹中讀取子句并判斷該子句是否是滿足。

2.如權利要求1所述的基于可編程邏輯的硬件SAT求解器，其特征在于，所述FPGA模塊還包括緩存模塊、隨機數產生模塊和循環控制模塊；

所述FPGA模塊在指定次數內根據預存的概率分布數據翻轉變元，具體包括：

循環控制模塊在指定次數內循環執行下列步驟：

從所述第二存儲模塊讀取不可滿足子句，暫存至所述緩存模塊；

在所述緩存模塊中將不可滿足子句的文字進行翻轉，所述計數器模塊計算各個變元翻轉后的break-value值，并將break-value排序；

將各變元排序后的break-value值與所述概率映射表進行比對，如果變元的break-value值存在于概率映射表中，所述隨機數產生模塊產生隨機數，所述變元翻轉模塊選擇隨機數對應的break-value值對應的變元進行翻轉；如果變元的break-value值不存在于概率映射表中，則所述變元翻轉模塊選擇最小的break-value值對應的變元進行翻轉；

將變元翻轉后的子句存儲到FIFO樹；

所述第二評估模塊從FIFO樹中讀取子句并判斷該子句是否是可滿足；

將不可滿足子句發送至第二存儲模塊。

3.如權利要求2所述的基于可編程邏輯的硬件SAT求解器，其特征在于，所述FPGA模塊還包括輸出模塊；

所述判斷CNF公式是否可滿足，具體包括：

所述循環控制模塊執行完指定次數后，所述第二存儲模塊和所述FIFO樹的最后一級FIFO均無不可滿足子句，則所述輸出模塊輸出所述CNF公式可滿足，否則所述輸出模塊輸出所述CNF公式不可滿足。

4.如權利要求1所述的基于可編程邏輯的硬件SAT求解器，其特征在于，所述CNF公式的格式為DIMACS格式。

5.如權利要求1所述的基于可編程邏輯的硬件SAT求解器，其特征在于，所述概率映射表預先存儲出現概率最高的對應的若干組break-value值。