[發(fā)明專利]一種布爾可滿足性求解器中學(xué)習子句的刪除方法及布爾可滿足性求解器

在審

• 申請?zhí)枺?/td>: 202110152277.6
• 申請日: 2021-02-03
• 公開（公告）號: CN112800681A
• 公開（公告）日: 2021-05-14
• 發(fā)明（設(shè)計）人: 畢舜陽;劉美華;張巖;黃國勇;屈璋
• 申請（專利權(quán)）人: 國微集團（深圳）有限公司
• 主分類號: G06F30/27
• 分類號: G06F30/27;G06F30/3308;G06N20/00
• 代理公司: 深圳市康弘知識產(chǎn)權(quán)代理有限公司 44247
• 代理人: 尹彥

本發(fā)明公開了一種布爾可滿足性求解器中學(xué)習子句的刪除方法及布爾可滿足性求解器，所述方法包括：在求解的過程中生成多個學(xué)習子句，并對每個學(xué)習子句的使用次數(shù)及LBD值進行記錄；當觸發(fā)學(xué)習子句刪除條件時，根據(jù)學(xué)習子句的使用次數(shù)和LBD值對學(xué)習子句進行刪減。采用本發(fā)明的技術(shù)方案，可提高學(xué)習子句的質(zhì)量，提升求解器的運行效率。

技術(shù)領(lǐng)域

本發(fā)明涉及電子設(shè)計自動化(Electronic Design Automation，EDA)領(lǐng)域，尤其涉及一種布爾可滿足性求解器中學(xué)習子句的刪除方法及布爾可滿足性求解器。

背景技術(shù)

布爾可滿足性問題是計算機科學(xué)領(lǐng)域的核心問題之一，其廣泛應(yīng)用于電子設(shè)計自動化、集成電路形式驗證、模型驗證等領(lǐng)域，一些工業(yè)領(lǐng)域的現(xiàn)實問題常常轉(zhuǎn)化為可滿足性問題進行求解。在可滿足性問題中，問題的輸入是一個合取范式(CNF)，合取范式由子句構(gòu)成，子句和子句之間以布爾運算“與”的形式連接，而構(gòu)成子句的是文字，文字和文字之間以布爾運算“或”的形式連接，文字為變量本身或變量的“非”。布爾可滿足性問題求解即為找到一組包含所有變量的解使得整個問題滿足，如果找不到這樣的解，則輸出該問題不可滿足。例如：對于這樣一個合取范式：子句為和變量為a、b、c，對應(yīng)的文字即為c、當a＝0、b＝0、c＝0時，該合取范式就是可滿足的，相反地，如果找不到這樣的解，則說明該合取范式不可滿足。

作為直接影響可滿足性問題求解時間的決定因素，求解器算法一直是該問題研究的重點。求解器算法按照框架主要分為三種：完備算法、不完備算法和混合算法，其中完備算法以現(xiàn)在主流的CDCL算法為主。近年來出現(xiàn)了一批以CDCL為算法框架的高效求解器，Glucose求解器就是其中最重要的代表之一，該求解器應(yīng)用的LBD學(xué)習子句刪除策略，大幅度提升了算法的求解性能。其中，Glucose求解器的主要求解過程分為六步，分別為預(yù)處理，分支啟發(fā)，布爾約束傳播，沖突分析及學(xué)習子句生成，學(xué)習子句刪除和重啟。Glucose求解器的簡要工作流程大致如下：先對讀入的CNF文件進行預(yù)處理，旨在化簡冗余子句，之后會根據(jù)分支啟發(fā)策略選擇一個文字賦值，并使其滿足，由于該文字的賦值可以推導(dǎo)出其他文字的賦值，繼而導(dǎo)致更多文字的賦值，由此產(chǎn)生的循環(huán)賦值過程即為布爾約束傳播。在傳播過程中遇到?jīng)_突的子句會進行沖突分析，并生成學(xué)習子句，以此保證下次不會產(chǎn)生相同的沖突，同時返回導(dǎo)致沖突產(chǎn)生的賦值層，重新開始賦值。由于在求解的過程中，直到求解結(jié)束，每一次沖突都會產(chǎn)生新的學(xué)習子句，學(xué)習子句會大量的累積并占用系統(tǒng)空間，因此，學(xué)習子句積累到一定數(shù)目會被刪除，用以釋放空間，提高搜索效率。

Glucose求解器中的LBD(Literals Blocks Distance，文字塊距離)策略可簡要概括為一種評價學(xué)習子句質(zhì)量的標準，該策略通過計算每個學(xué)習子句的LBD值，然后將學(xué)習子句的LBD值排序，進而將LBD大的學(xué)習子句刪除。LBD值反映了在學(xué)習子句中所有文字所在的賦值層數(shù)。一個學(xué)習子句的LBD值越小意味著這個子句被賦值的難度越小，因此變量之間的約束就更加緊密，當再次遇到?jīng)_突時，就可以高效的避免重復(fù)的沖突發(fā)生。但在經(jīng)實際的多組測試例子運行之后發(fā)現(xiàn)，經(jīng)過LBD排序篩選得到的學(xué)習子句并非都能在沖突分析時被多次用到，詳細數(shù)據(jù)如表一所示：

表一

通過表一中的三個測試例子可以看出，被使用1次以下(包含1次)的學(xué)習子句保留率在40％以上，因此LBD策略保留的學(xué)習子句并不都是高效的學(xué)習子句。

發(fā)明內(nèi)容

本發(fā)明的目的是針對現(xiàn)有技術(shù)的布爾可滿足性求解器中的學(xué)習子句刪除策略保留的學(xué)習子句并不都是高效的學(xué)習子句的技術(shù)問題，本發(fā)明提出一種布爾可滿足性求解器中學(xué)習子句的刪除方法及布爾可滿足性求解器。

本發(fā)明實施例中，提供了一種布爾可滿足性求解器中學(xué)習子句的刪除方法，其包括：

在求解的過程中生成多個學(xué)習子句，并對每個學(xué)習子句的使用次數(shù)及LBD值進行記錄；