[發明專利]一種基于二元域的高效決策判定方法在審

申請號：	201810788520.1	申請日：	2018-07-18
公開（公告）號：	CN108984473A	公開（公告）日：	2018-12-11
發明（設計）人：	劉江;周鴻昊	申請（專利權）人：	中國科學院重慶綠色智能技術研究院
主分類號：	G06F17/12	分類號：	G06F17/12
代理公司：	上海光華專利事務所(普通合伙) 31219	代理人：	尹麗云
地址：	400714 ***	國省代碼：	重慶;50
權利要求書：	查看更多	說明書：	查看更多
摘要：
搜索關鍵詞：	二元域決策判定求解可滿足性問題線性方程組人工智能電路設計計算效率命題邏輯求解問題公式化常數解判定檢測轉化應用
鉆瓜網技術展會專利詞庫專利權人專利榜在售專利公布日期熱門專利

【說明書】：

本發明提供一種基于二元域的高效決策判定方法，通過將布爾命題邏輯的可滿足性問題轉化為一個線性方程組的求解問題后，利用0?1解的性質，在二元域上求解，當方程在二元域上有多解時，求出某些變量的常數解，代入公式化簡后再次求解，直到求出所有變量的值，本發明可以廣泛應用于數理邏輯、人工智能、電路設計與檢測等領域，計算效率，增強了判定方法的實用性。

技術領域

本發明涉及計算機領域，尤其涉及一種基于二元域的高效決策判定方法。

背景技術

可滿足性問題(SAT問題)在數理邏輯、人工智能、電路設計與檢測等領域具有廣闊的應用背景。SAT問題是第一個NP完全問題，目前沒有多項式時間的完備求解算法。

目前，現有技術中比較流行的SAT求解算法大部分基于搜索和推理的DPLL算法。CDCL算法在沖突分析與子句學習、非時序回溯、重啟、數據結構等方面做了一系列改進。完備的DPLL類算法的最壞時間復雜度是指數級別的，所以研究者對搜索空間進行剪枝，即局部搜索。局部搜索是不完備的，當搜索不到解時，無法判定布爾公式是否可滿足。此外，不完備算法還有基于優化的算法、基于統計物理的算法等。基于優化的算法易陷入局部最優，而基于統計物理的Survey Propagation算法收斂條件比較苛刻。

發明內容

鑒于以上所述現有技術的缺點，本發明提供一種基于二元域的高效決策判定方法，以解決上述技術問題。

本發明提供的基于二元域的高效決策判定方法，包括：

S1.根據決策判斷問題建立布爾命題邏輯公式，并將所述布爾命題邏輯公式轉化為1-in-3-SAT公式；

S2.將所述1-in-3-SAT公式轉化為等價的線性布爾系統；

S3.對所述等價的線性布爾系統在二元域上進行求解，如果求解結果為無解，則輸出系統不相容，并終止；否則進入步驟S4；

S4.如果求解結果為每個子句中變元≤2，且求解結果為有解，則輸出系統相容，否則進入步驟S5；

S5：如果求解結果在二元域上解的個數不超過預設的閾值，則進入步驟S6；否則進入步驟S7；

S6：驗證求解結果是否存在1-in-3-SAT的解，如果存在，則輸出系統相容，并終止；如果不存在，則輸出系統不相容，并終止；

S7：如果求解結果為在二元域上有常數解，則進入步驟S8；如果沒有常數解，則輸出無法判定；

S8：根據所述常數解確定變量的值，對所述1-in-3-SAT公式進行化簡后，進入步驟S2。

本發明通過將LAF第一次線性化得到的方程組，在二元域上求解，此方法可得到部分變量的常數解，代入得到簡化公式，并依此迭代。整個過程在多項式時間內完成，可以提高布爾命題邏輯公式的可滿足性判定速度。