模型計數(shù)（model counting,#SAT）問題旨在計算給定的公式集合中所有模型的個數(shù),絕大部分計算復(fù)雜度為#P的問題均可以在多項式時間內(nèi)歸約為模型計數(shù)問題。在人工智能領(lǐng)域,許多計算復(fù)雜度高于NP的問題均可轉(zhuǎn)化為模型計數(shù)問題進行求解。因此,研究模型計數(shù)問題求解技術(shù)對可以與模型計數(shù)問題相互轉(zhuǎn)化的領(lǐng)域有著重要意義。然而,現(xiàn)有的精確模型計數(shù)求解算法對大規(guī)模問題求解能力較為低下,而且對于目前的許多問題來說,求出精確的模型數(shù)是不必要的,因此近似模型計數(shù)求解技術(shù)被提出。其中最有潛力的方法之一就是基于異或約束進行近似求解。該求解方法的本質(zhì)是基于采樣的思想,利用平均長度為變量數(shù)一半的異或約束對解空間進行削減,待解空間削減到足夠小后,利用精確求解技術(shù)對其求解從而得到精確模型數(shù),最后通過該解空間與整體解空間的比例關(guān)系估算整體解空間的近似模型數(shù)。通過對現(xiàn)有的近似求解算法的深入研究,本文提出了一種新的結(jié)合有界求解策略與可控隨機策略的近似#SAT求解算法。由于異或約束在解空間較小時分割不夠精確,有界求解策略通過限制應(yīng)用異或約束的解空間規(guī)模有效地提升了求解算法的精確度�？煽仉S機策略利用骨架變量以及變量之間的... 

【文章來源】：吉林大學吉林省 211工程院校 985工程院校 教育部直屬院校

【文章頁數(shù)】：64 頁

【學位級別】：碩士

【部分圖文】：

#KiF與#KiF的差異對比

第4章實驗結(jié)果與分析23步驟1.調(diào)用三個算法各自生成異或約束的部分生成異或約束；步驟2.添加到合取范式F中；步驟3.調(diào)用SAT求解器對F進行求解；步驟4.重復(fù)步驟1-3，直到步驟3出現(xiàn)合取范式F不可滿足，重置合取范式F為原始狀態(tài)，記錄當前消耗的時間t(s)，以及添加的異或約束的總數(shù)XOR_NUM，則XOR_NUM/t為單位時間內(nèi)添加的異或約束的數(shù)量。以上三個求解器均采用Cryptominisat[37]作為后端的SAT求解器。此外，為消除AMCX_BC中預(yù)處理對實驗結(jié)果的影響，實驗也為ApproxMC2和STAC_CNF分別添加了與AMCX_BC相同的預(yù)處理策略。在實驗中，每個測試樣例將重復(fù)100次上述過程，所獲得的結(jié)果為單位時間內(nèi)添加的異或約束的數(shù)量。需要說明的是，預(yù)處理的時間消耗沒有算在整體時間內(nèi)。具體實驗結(jié)果如圖4-1所示。圖4-1.單位時間內(nèi)添加的異或約束數(shù)量比較圖4-1的橫坐標代表測試樣例，縱坐標代表代為單位時間內(nèi)添加的異或約束的數(shù)量。為便于比較，縱坐標采用對數(shù)刻度，120個測試樣例按照ApproxMC2withpreprocessing曲線遞增排序。從總體上來看，預(yù)處理對于單位時間內(nèi)能夠添加的異或約束數(shù)量的提升并不明顯，主要起作用的應(yīng)為可控隨機策略。針對編號

AMCX_BC,ApproxMC2與STAC_CNF的求解時間比較


本文編號：3543826