[發(fā)明專利]一種基于GPU的模型計數(shù)及其約束的求解方法

在審

• 申請?zhí)枺?/td>: 202010908484.5
• 申請日: 2020-09-02
• 公開（公告）號: CN112131583A
• 公開（公告）日: 2020-12-25
• 發(fā)明（設(shè)計）人: 宋富;高鵬飛;謝弘毅
• 申請（專利權(quán)）人: 上海科技大學(xué)
• 主分類號: G06F21/60
• 分類號: G06F21/60;G06F21/62
• 代理公司: 上海申匯專利代理有限公司 31001
• 代理人: 徐俊

1.一種基于GPU的模型計數(shù)及其約束的求解方法，其特征在于，包括以下步驟：

步驟1、對于任意給定一個或一組邏輯公式表示的模型計數(shù)或模型計算約束問題，利用編譯技術(shù)將公式翻譯為中間結(jié)果表達(dá)式；

步驟2、根據(jù)邏輯公式變量數(shù)和GPU的架構(gòu)信息，將變量劃分為三類：CPU枚舉變量、GPU線程標(biāo)識符對應(yīng)變量、GPU線程枚舉變量；

步驟3、根據(jù)變量劃分，通過遍歷邏輯公式的中間結(jié)果形式，自動生成GPU程序，從而將模型計數(shù)及其約束問題轉(zhuǎn)化為GPU程序執(zhí)行，調(diào)用GPU程序編譯器進行編譯并運行GPU可執(zhí)行文件，根據(jù)模型計數(shù)或模型計算約束問題給出執(zhí)行結(jié)果，其中，GPU程序生成過程包括以下步驟：

步驟3.1、對邏輯公式中的邏輯運算符，判斷是不是GPU程序支持的運算符，如果是GPU中不支持的運算符，則在GPU程序中生成一個對應(yīng)的__device__類型的函數(shù)實現(xiàn)該運算，供后續(xù)調(diào)用；如果是GPU程序中支持的運算符，則直接使用GPU程序中對應(yīng)的運算符；

步驟3.2、對每一個邏輯表達(dá)式，通過遍歷其中間表示形式，在GPU程序中生成一個對應(yīng)的__device__類型的函數(shù)用于計算邏輯表達(dá)式的值，其參數(shù)分別是CPU和GPU枚舉變量的一組具體值以及線程標(biāo)識符，表達(dá)式的計算通過GPU內(nèi)置的運算符和步驟3.1中定義的__device__類型的函數(shù)實現(xiàn)；

步驟3.3、在GPU程序中生成一個核函數(shù)，該核函數(shù)枚舉GPU線程枚舉變量的取值，對每一組取值，調(diào)用對應(yīng)邏輯公式的__device__函數(shù)計算所有邏輯公式的具體值；在數(shù)組中以所有邏輯公式的值為索引的模型數(shù)量加1；

步驟3.4、在GPU程序中生成一個主函數(shù)，該主函數(shù)設(shè)置GPU流處理器線程網(wǎng)絡(luò)模式，將核函數(shù)布置到線程網(wǎng)絡(luò)，初始化保存模型計數(shù)的數(shù)組使得每個索引的模型數(shù)量為0；枚舉CPU枚舉變量的取值，對每一組枚舉的變量取值，調(diào)用核函數(shù)并把變量取值以參數(shù)形式傳遞給核函數(shù)；

如果是計算模型計數(shù)值，則等枚舉完所有CPU枚舉變量的取值后，返回保存模型數(shù)量的數(shù)組；如果是模型計數(shù)約束求解問題，則在每次枚舉CPU枚舉變量的取值后，判定約束是否成立，一旦判定為不成立，立刻返回不成立結(jié)果；等枚舉完所有CPU枚舉變量的取值后還沒有出現(xiàn)約束不成立情況，則判定為約束成立。

2.如權(quán)利要求1所述的一種基于GPU的模型計數(shù)及其約束的求解方法，其特征在于，所述中間結(jié)果表達(dá)式采用抽象語法樹或程序依賴圖。

3.如權(quán)利要求1所述的一種基于GPU的模型計數(shù)及其約束的求解方法，其特征在于，采用GPU線程標(biāo)識符枚舉GPU線程標(biāo)識符對應(yīng)變量的取值。