资料下载
基于奖励机制的SAT求解器分支策略综述
分享资料个
分支决策是CDCL（ Conflict Driven Clause Learning）求解器一个十分关键的环节，一个妤的分支策略可以减少分支决策次数进而提高SAT求解器的效率。目前，先进的分支策略大都结合了冲突分析过程，但分支策略对参与冲突分析的变量奖励方法有所不同，因此所挑选出的决策变量会有所差异。文中考虑到决策变量总是在未赋值变量中选取的这一重要事实，在EVSIDS（ Exponential Variable State Independent Decaying Sum）分支策略的基础上提出了一种新的分支策略，称为基于奖励机制的分支策略（简称RACT分支策略）。RACT分攴策略对冲突分析中被撤销赋值的变量再次給予奖励，以増大未赋值变量中频繁参与冲突分析的变量被选择为分支变量的可能性。最后，将所提岀的分攴策略嵌入到 Glucose4.1求解器中以形成新的求解器 Glucosea.1十RACT，以2017年SAT竞赛中的350个实例为实验数据集来测试RACT分支策略的有效性。实验结果表明，求解器 Glucose4.1十RACT比原版求解器能求解出更多的实例个数，尤其在求解可满足实例的个数上增加了%，此外在求解350个竞赛实例上所花费的总时间较 Glucose4.1减少了3.9%，以上实验数据均说明所提分支策略可以有效减少搜索树的分支决策次数并给出正确的搜索空间，进而提高了SAT求解器的求解能力。
声明：本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人，不代表电子发烧友网立场。文章及其配图仅供工程师学习之用，如有内容侵权或者其他违规问题，请联系本站处理。 举报投诉
- 相关下载
- 相关文章
