在現(xiàn)有基于沖突學習子句的求解器中,重啟和變量相位存儲技術(shù)的頻繁應(yīng)用,導致重啟之后產(chǎn)生大量重復變量賦值序列,在求解過程中對變量重復賦值會浪費求解資源.本文提出一種基于識別重復路徑的動態(tài)決策策略.首先,檢測搜索過程中產(chǎn)生的重復賦值變量序列,算法中參數(shù)依據(jù)子句數(shù)與變元數(shù)的比率而動態(tài)變化;其次,更新參與沖突次數(shù)最多的變量的活躍值,選擇合適的分支決策變量,改變變量賦值序列.本文基于國際SAT競賽中知名求解器Glucose3.0,MapleCOMSPS,Glucose4.1以及Lingeling,分別實現(xiàn)了改進算法——DDIDT.實驗結(jié)果可得,改進求解器Glucose_DDIDT相比Glucose3.0降低決策數(shù)為11.2%～61.6%,且Glucose_DDIDT求解難度較大實例的個數(shù)提高了63.9%.針對求解2015年到2017年SAT競賽的應(yīng)用類型的實例,Glucose_DDIDT相比Glucose3.0的求解個數(shù)增長了6.0%;改進求解器MapleCOMSPS_DDIDT相比MapleCOMSPS求解個數(shù)提高了...

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

【文章目錄】：
1 引言
2 基礎(chǔ)知識
    2.1 基本概念
    2.2 CDCL算法
    2.3 重啟策略
        2.3.1 靜態(tài)重啟策略
        2.3.2 動態(tài)重啟策略
3 基于識別重復路徑的決策策略
    3.1 重復賦值序列
    3.2 識別重復賦值序列
    3.3 動態(tài)改變賦值序列
4 實驗與結(jié)果分析
    4.1 求解單個實例
    4.2 求解不同類型實例
    4.3 實驗結(jié)果
5 總結(jié)
Background



本文編號：3872832