加权决策变量提升SAT求解器效率：一种新的分支策略

本文主要探讨了一种旨在提高冲突求解器（Conflict-Driven Clause Learning, CDCL）在解决可满足性（Satisfiability, SAT）问题时效率的新型分支策略。该策略的核心是基于加权决策变量决策层，它通过以下几个步骤来优化决策过程： 1. 考虑决策变量的频率与层次：策略首先依据布尔约束传播（Boolean Constraint Propagation, BCP）中的回溯和重启机制，重视那些在解空间探索中出现频率较高且处于较低决策层的变量。这样可以优先处理那些对问题影响可能更大的变量。 2. 赋予权重：由于不同变量的选择对解决问题的影响程度不同，策略会根据它们的被选择次数和所在的决策层赋予不同的权重。这种加权方法使得决策过程更加精细，有利于减少无效搜索。 3. 冲突分析与奖励得分：结合冲突分析，策略会根据变量在冲突解决过程中的作用给予不同的奖励得分，进一步优化决策变量的选择。这有助于避免过多的冲突，提升求解效率。 4. 策略比较与实验验证：作者将新策略与VSIDS（Variable State Independent Decaying Summaries）和EVIDS（Evidence Guided Variable Selection）等传统策略进行了对比。通过大量的SATLIB（Satisfiability Little Information Bank）实例测试，结果显示新策略能够有效地减少冲突次数和求解所需CPU时间，从而显著提高了CDCL求解器的整体性能。 关键词：决策层、加权、重启、决策变量、冲突。这篇文章的研究成果对于理解和改进SAT问题的求解算法具有重要意义，特别是在处理大规模复杂问题时，其潜在的应用价值不可忽视。