[發明專利]一種布爾可滿足性驗證方法及系統在審
| 申請號： | 202011521824.5 | 申請日： | 2020-12-21 |
| 公開（公告）號： | CN112507656A | 公開（公告）日： | 2021-03-16 |
| 發明（設計）人： | 李鵬飛;劉美華;張巖;黃國勇 | 申請（專利權）人： | 國微集團（深圳）有限公司 |
| 主分類號： | G06F30/398 | 分類號： | G06F30/398 |
| 代理公司： | 深圳市康弘知識產權代理有限公司 44247 | 代理人： | 尹彥 |
| 地址： | 518000 廣東省深圳市南山區粵*** | 國省代碼： | 廣東;44 |
| 權利要求書： | 查看更多 | 說明書： | 查看更多 |
| 摘要： | |||
| 搜索關鍵詞： | 一種 布爾 滿足 驗證 方法 系統 | ||
1.一種布爾可滿足性驗證方法，其特征在于，包括：對CNF實例中每個變元的權重進行計算，選擇所述權重最高的變元作為SAT求解器的第一個分支變元。
2.如權利要求1所述的布爾可滿足性驗證方法，其特征在于，對CNF實例中每個變元的權重進行計算，包括：
步驟S1：將CNF實例中的所有文字以子句為單位讀入一個二維容器之中；
步驟S2：分別計算CNF實例中每個變元的權重。
3.如權利要求2所述的布爾可滿足性驗證方法，其特征在于，計算CNF實例中每個變元的權重，包括：
對存放CNF子句的二維容器進行遍歷，
若某變元出現在某個子句中，則計算其當前權重：
Weight = 1/當前子句文字數，
若此變元在后面的某個子句中再次出現，則對其權重進行累加：
Weight = Weight + 1/當前子句文字數，
直到所有子句遍歷完成，得到一個存放所有變元最終權重的列表。
4.如權利要求3所述的布爾可滿足性驗證方法，其特征在于，選擇所述權重最高的變元作為第一個分支變元，包括：
步驟S3：找到所述列表中擁有最高權重的變元；
步驟S4：將權重最高的變元的活性初始化為一個大于0的值，將其它變元的活性初始化為0。
5.如權利要求1所述的布爾可滿足性驗證方法，其特征在于，所述SAT求解器采用分支啟發式策略對CNF實例進行求解。
6.一種布爾可滿足性驗證系統，其特征在于，對CNF實例進行布爾可滿足性驗證時，采用如權利要求1-5任一項所述的布爾可滿足性驗證方法。
該專利技術資料僅供研究查看技術是否侵權等信息，商用須獲得專利權人授權。該專利全部權利屬于國微集團（深圳）有限公司，未經國微集團（深圳）有限公司許可，擅自商用是侵權行為。如果您想購買此專利、獲得商業授權和技術合作，請聯系【客服】
本文鏈接：http://www.szxzyx.cn/pat/books/202011521824.5/1.html，轉載請聲明來源鉆瓜專利網。
