基于獎(jiǎng)勵(lì)機(jī)制的SAT求解器分支策略綜述

　　分支決策是CDCL（ Conflict Driven Clause Learning）求解器一個(gè)十分關(guān)鍵的環(huán)節(jié)，一個(gè)妤的分支策略可以減少分支決策次數(shù)進(jìn)而提高SAT求解器的效率。目前，先進(jìn)的分支策略大都結(jié)合了沖突分析過(guò)程，但分支策略對(duì)參與沖突分析的變量獎(jiǎng)勵(lì)方法有所不同，因此所挑選出的決策變量會(huì)有所差異。文中考慮到?jīng)Q策變量總是在未賦值變量中選取的這一重要事實(shí)，在EVSIDS（ Exponential Variable State Independent Decaying Sum）分支策略的基礎(chǔ)上提出了一種新的分支策略，稱為基于獎(jiǎng)勵(lì)機(jī)制的分支策略（簡(jiǎn)稱RACT分支策略）。RACT分攴策略對(duì)沖突分析中被撤銷賦值的變量再次給予獎(jiǎng)勵(lì)，以増大未賦值變量中頻繁參與沖突分析的變量被選擇為分支變量的可能性。最后，將所提岀的分攴策略嵌入到 Glucose4.1求解器中以形成新的求解器 Glucosea.1十RACT，以2017年SAT競(jìng)賽中的350個(gè)實(shí)例為實(shí)驗(yàn)數(shù)據(jù)集來(lái)測(cè)試RACT分支策略的有效性。實(shí)驗(yàn)結(jié)果表明，求解器 Glucose4.1十RACT比原版求解器能求解出更多的實(shí)例個(gè)數(shù)，尤其在求解可滿足實(shí)例的個(gè)數(shù)上增加了%，此外在求解350個(gè)競(jìng)賽實(shí)例上所花費(fèi)的總時(shí)間較 Glucose4.1減少了3.9%，以上實(shí)驗(yàn)數(shù)據(jù)均說(shuō)明所提分支策略可以有效減少搜索樹(shù)的分支決策次數(shù)并給出正確的搜索空間，進(jìn)而提高了SAT求解器的求解能力。