[發(fā)明專利]變?cè)馁x值順序及賦值優(yōu)化算法、布爾可滿足性驗(yàn)證算法

在審

• 申請(qǐng)?zhí)枺?/td>: 202011634036.7
• 申請(qǐng)日: 2020-12-31
• 公開（公告）號(hào): CN112733350A
• 公開（公告）日: 2021-04-30
• 發(fā)明（設(shè)計(jì)）人: 劉美華;屈璋;張巖;黃國勇;金玉豐
• 申請(qǐng)（專利權(quán)）人: 國微集團(tuán)（深圳）有限公司
• 主分類號(hào): G06F30/20
• 分類號(hào): G06F30/20;G06F11/36
• 代理公司: 深圳市康弘知識(shí)產(chǎn)權(quán)代理有限公司 44247
• 代理人: 尹彥

1.一種分支啟發(fā)的變?cè)馁x值順序優(yōu)化算法，其特征在于，至少一個(gè)變?cè)捎靡韵虏襟E確定賦值順序：

步驟1，將當(dāng)前待賦值的變?cè)鳛楫?dāng)前變?cè)?/p>

步驟2，搜索與當(dāng)前變?cè)瑫r(shí)出現(xiàn)在同一子句中的關(guān)聯(lián)變?cè)?/p>

步驟3，累計(jì)所述關(guān)聯(lián)變?cè)c當(dāng)前變?cè)瑫r(shí)出現(xiàn)在同一子句中的次數(shù)；

步驟4，選擇次數(shù)最少的關(guān)聯(lián)變?cè)鳛槔^當(dāng)前變?cè)蟮拇x值的變?cè)?/p>

2.如權(quán)利要求1所述的分支啟發(fā)的變?cè)馁x值順序優(yōu)化算法，其特征在于，所述步驟4執(zhí)行完畢后返回步驟1，直至同一字句的所有的變?cè)馁x值順序確定。

3.如權(quán)利要求2所述的分支啟發(fā)的變?cè)馁x值順序優(yōu)化算法，其特征在于，所述當(dāng)前待賦值的變?cè)獮榉种l(fā)的第一個(gè)待賦值的變?cè)蛘邽樽泳涞牡谝粋€(gè)待賦值的變?cè)?/p>

4.如權(quán)利要求3所述的分支啟發(fā)的變?cè)馁x值順序優(yōu)化算法，其特征在于，所述分支啟發(fā)的第一個(gè)待賦值的變?cè)ㄟ^對(duì)CNF文件每個(gè)變?cè)臋?quán)重進(jìn)行計(jì)算，選擇所述權(quán)重最高的變?cè)鳛镾AT求解器的第一個(gè)待賦值的變?cè)?/p>

5.如權(quán)利要求4所述的分支啟發(fā)的變?cè)馁x值順序優(yōu)化算法，其特征在于，所述對(duì)CNF文件中每個(gè)變?cè)臋?quán)重進(jìn)行計(jì)算，包括：

將CNF文件中的所有文字以子句為單位讀入一個(gè)二維容器之中；

對(duì)所述存放子句的二維容器進(jìn)行遍歷分別計(jì)算CNF文件中每個(gè)待賦值的變?cè)臋?quán)重。

6.如權(quán)利要求5所述的分支啟發(fā)的變?cè)馁x值順序優(yōu)化算法，其特征在于，計(jì)算每個(gè)待賦值的變?cè)臋?quán)重具體包括：

在遍歷子句的過程中，當(dāng)某個(gè)待賦值的變?cè)霈F(xiàn)在某個(gè)子句中，則根據(jù)公式計(jì)算其當(dāng)前權(quán)重；

直至所有子句遍歷完成，得到所有待賦值的變?cè)臋?quán)重。

7.一種分支啟發(fā)的變?cè)馁x值優(yōu)化算法，其特征在于，采用如權(quán)利要求1至6任意一項(xiàng)所述的變?cè)馁x值順序優(yōu)化算法確定變?cè)馁x值順序，當(dāng)任意一個(gè)變?cè)馁x值順序被確定時(shí)，包括如下賦值步驟：

對(duì)待賦值的變?cè)M(jìn)行第一次賦值；

計(jì)算賦值以后所述待賦值的變?cè)诜种l(fā)中發(fā)生n次沖突的第一時(shí)間；

將第一次賦值的值進(jìn)行取反并以取反后的值對(duì)待賦值的變?cè)M(jìn)行第二次賦值；

計(jì)算賦值以后所述待賦值的變?cè)诜种l(fā)中發(fā)生n次沖突的第二時(shí)間；

比較第一時(shí)間和第二時(shí)間，選擇時(shí)間短的那次賦值的值對(duì)待賦值的變?cè)M(jìn)行賦值。

8.如權(quán)利要求7所述的分支啟發(fā)的變?cè)馁x值優(yōu)化算法，其特征在于，所述待賦值的變?cè)牡谝淮钨x值的值為1。

9.一種布爾可滿足性驗(yàn)證算法，其特征在于，在對(duì)CNF文件進(jìn)行布爾可滿足性驗(yàn)證時(shí)，采用如權(quán)利要求7或8所述的分支啟發(fā)的變?cè)馁x值優(yōu)化算法對(duì)各個(gè)變?cè)M(jìn)行賦值。