命題邏輯公式的可滿足性問題(SAT問題)是指給出一個(gè)合取范式,判斷是否存在一組賦值使得這個(gè)合取范式可滿足。SAT問題是計(jì)算機(jī)科學(xué)與工程、人工智能、計(jì)算機(jī)視覺和計(jì)算機(jī)輔助設(shè)計(jì)等領(lǐng)域的一個(gè)核心問題,它也是第一個(gè)被證明的NP完全(Non-Deterministic Polynomial-Complete,NPC)問題。正因?yàn)槿绱?研究SAT問題并提高求解器的效率是很有價(jià)值的。求解SAT問題的算法分為完備算法和不完備算法。完備算法的特點(diǎn)是在問題可滿足時(shí),給出一個(gè)模型;不可滿足時(shí),給出證明�；谕陚渌惴ǖ膬�(yōu)點(diǎn),本文以CDCL(Conflict Driven Clause Learning,CDCL)算法為框架,研究CDCL算法的以下主要流程:決策、沖突分析、學(xué)習(xí)子句和回溯之間的關(guān)系。SAT求解器的成功絕大多數(shù)歸因于從錯(cuò)誤賦值中學(xué)習(xí)的能力、快速地刪除搜索空間以及首先集中在那些“重要”變量中^[1]。故本文集中在CDCL算法中的決策和沖突分析上,取得的主要研究結(jié)果如下:1.當(dāng)一個(gè)命題邏輯中的邏輯公式以CNF的形式輸入到數(shù)據(jù)庫時(shí),從中選擇“重要”變量的依據(jù)是變量出現(xiàn)的次數(shù)和包含該變...

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

【學(xué)位級別】：碩士

【文章目錄】：
摘要
Abstract
第1章 緒論
    1.1 研究背景和意義
    1.2 SAT問題國內(nèi)外研究現(xiàn)狀
    1.3 本文研究的內(nèi)容和結(jié)構(gòu)安排
第2章 SAT問題基本理論
    2.1 算法復(fù)雜度
    2.2 P問題、NP問題和NPC問題
    2.3 SAT問題基本定義
    2.4 本章小結(jié)
第3章 CDCL算法研究進(jìn)展
    3.1 DPLL算法
    3.2 CDCL算法
        3.2.1 CDCL算法偽代碼
        3.2.2 analyze-conflict()和Backtrack()
    3.3 決策啟發(fā)式策略
    3.4 本章小結(jié)
第4章 基于VSIDS改進(jìn)的分支啟發(fā)式策略
    4.1 CLVDL分支啟發(fā)式策略
        4.1.1 變量初始記分
        4.1.2 變量“碰撞”記分
    4.2 CLVDL算法步驟
    4.3 本章小結(jié)
第5章 算法分析及實(shí)驗(yàn)結(jié)果
    5.1 算法分析
    5.2 測試相關(guān)說明
    5.3 測試結(jié)果比較
        5.3.1 SAT競賽結(jié)果比較
        5.3.2 SATLIB測試結(jié)果比較
    5.4 本章小結(jié)
第6章 總結(jié)與展望
    6.1 總結(jié)
    6.2 展望
致謝
參考文獻(xiàn)
攻讀碩士學(xué)位期間發(fā)表的論文及參與的科研工作
    1.碩士期間發(fā)表的論文
    2.碩士期間參與的科研項(xiàng)目



本文編號：3842149