[發明專利]一種基于二元域的高效決策判定方法在審
| 申請號： | 201810788520.1 | 申請日： | 2018-07-18 |
| 公開（公告）號： | CN108984473A | 公開（公告）日： | 2018-12-11 |
| 發明（設計）人： | 劉江;周鴻昊 | 申請（專利權）人： | 中國科學院重慶綠色智能技術研究院 |
| 主分類號： | G06F17/12 | 分類號： | G06F17/12 |
| 代理公司： | 上海光華專利事務所(普通合伙) 31219 | 代理人： | 尹麗云 |
| 地址： | 400714 *** | 國省代碼： | 重慶;50 |
| 權利要求書： | 查看更多 | 說明書： | 查看更多 |
| 摘要： | |||
| 搜索關鍵詞： | 二元域 決策判定 求解 可滿足性問題 線性方程組 人工智能 電路設計 計算效率 命題邏輯 求解問題 公式化 常數解 判定 檢測 轉化 應用 | ||
1.一種基于二元域的高效決策判定方法，其特征在于，包括：
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。
2.根據權利要求1所述的基于二元域的高效決策判定方法，其特征在于，所述1-in-3-SAT公式為：
所述等價的線性布爾系統為：
其中，變元X和U為方程的布爾變元，
將所述線性布爾系統記為：A·Y＝II，其中，A是線性布爾系統的系數矩陣，Y為變元X和U的列向量，II為所有坐標皆為單位1的列向量。
3.根據權利要求2所述的基于二元域的高效決策判定方法，其特征在于，所述求解結果為：
y0+k1y1+k2y2+...+kpyp
其中，其中y0為方程組的特解向量，k1y1+k2y2+...+kpyp為AY＝0的通解向量，
所述閾值為2t，當p≤t時，解的個數不大于2t，窮舉驗證求解結果是否存在1-in-3-SAT的解。
4.根據權利要求3所述的基于二元域的高效決策判定方法，其特征在于，在所述步驟S8中，如果有常數解Yi＝1，則在1-in-3-SAT公式中對應的布爾變元值為true；如果有常數解Yi＝0，則在1-in-3-SAT公式中對應的布爾變元值為false。
5.根據權利要求1所述的基于二元域的高效決策判定方法，其特征在于：所述布爾命題邏輯公式由布爾變量經過布爾運算迭代生成。
6.一種計算機可讀存儲介質，其上存儲有計算機程序，其特征在于：該程序被處理器執行時實現權利要求1至5中任一項所述方法。
7.一種電子終端，其特征在于，包括：處理器及存儲器；
所述存儲器用于存儲計算機程序，所述處理器用于執行所述存儲器存儲的計算機程序，以使所述終端執行如權利要求1至5中任一項所述方法。
該專利技術資料僅供研究查看技術是否侵權等信息，商用須獲得專利權人授權。該專利全部權利屬于中國科學院重慶綠色智能技術研究院，未經中國科學院重慶綠色智能技術研究院許可，擅自商用是侵權行為。如果您想購買此專利、獲得商業授權和技術合作，請聯系【客服】
本文鏈接：http://www.szxzyx.cn/pat/books/201810788520.1/1.html，轉載請聲明來源鉆瓜專利網。
