一種基于加權決策變量決策層的分支策略

摘要：為了提高CDCL求解器的求解效率,針對可滿足性(SAT)問題算法中決策變量的選擇問題,提出了一種基于加權決策變量決策層的分支策略。這個新策略的主要思想是:基于布爾約束傳播(BCP)過程中的回溯以及重啟機制,首先考慮變量作為決策變量的次數以及所在決策層;其次,由于被選擇的次數以及所在決策層不同,即占權重不同,對此進行加權;最后,結合沖突分析過程,對不同的變量給予不同的獎勵得分。將不同變量在新策略與VSIDS和EVIDS策略中的得分進行對比,采用SATLIB(SAT Little Information Bank)中的大量例子進行實驗測試,結果表明,新策略能夠減少沖突次數以及求解時間(cpu),提高了求解器的求解效率。