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

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

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



本文編號(hào)：3872832