标签：Branching CHB Weighted 变量 Heuristic 得分 冲突 multiplier 策略
1. CHB(conflict history-based branching heuristic)分支策略
1.1 奖励函数
- \(numConflicts\) 从搜索开始发生冲突的总次数
- \(lastConflict[v]\) 文字\(v\)在冲突分析出现，则\(lastConflict[v] = numConflicts\)
- \(multiplier\) 取值为1.0或0.9。\(multiplier=1.0\) 当分支、传播或断言的变量在传播后立即导致冲突时，将multiplier设置为1.0。这意味着变量对识别冲突有直接和显著的影响，因此应该给予更高的奖励，以增加将来选择该变量进行分支的可能性。 \(multiplier = 0.9\) 如果分支、传播或断言的变量在传播后没有立即导致冲突，则将multiplier设置为0.9。这表明变量对识别冲突的影响较小，因此应该给予较低的奖励。
\[r_v = \frac {multiplier}{numConflicts - lastConflict[v] + 1}
\]
1.2 文字得分
- \(Q[v]\)是一个浮点数
- 每个文字的\(Q[v]\)值进行搜索之前初始化为0
- \(\alpha\)初始值为0.4，后续每次冲突减少\(10^{-6}\)，直到减为0.06，后续保持不变。
\[Q[v] = (1 - \alpha)*Q[v] + \alpha*r_v
\]
1.3 CHB策略步骤
- 初始化
- 对于每个布尔变量，初始化一个浮点数Q分数(Q score)为0。
- 设置步长(step-size)α的初始值为0.4，并在每次冲突后减少\(10^{-6}\)，直到达到最小值0.06。
- 分支过程
- 在每次分支时，选择未分配的变量v，其Q分数最高，作为分支变量。
- 分配一个真值（true或false）给选定的变量，通常基于极性启发式，例如阶段保存（phase saving）。
- 传播和冲突处理
- 进行布尔约束传播。
- 如果传播导致冲突，确定multiplier的值:
- 如果变量在传播后立即导致冲突，则multiplier设置为1.0。
- 如果变量在传播后没有立即导致冲突，则multiplier设置为0.9。
- 对于参与传播的每个变量，更新其Q分数，使用[[#1.2 文字得分]]中提到的公式，其中\(r_v\)使用[[#1.1 奖励函数]]中提到的公式。
1.4 伪码
1.5 CHB策略与VSIDS策略的区别
- VSIDS策略只会在冲突分析中更新变元的得分，而CHB策略会在一个文字被赋值时(即该文字做为分支变元被赋值、单子句传播被赋值等)更新其得分。
- VSIDS策略会周期性的对所有文字的得分乘以衰减因子，但是CHB策略只会在一个文字被赋值时衰减该文字的得分。
- VSIDS策略对文字的得分进行bump是固定的，而CHB策略不是固定的，bump给文字的值是奖励函数计算出的得分。并且CHB策略bump的值(reward value)是基于历史冲突的，而VSIDS策略bump的值只基于当前冲突，原始VSIDS策略该bump值为常量1。
2. 其他
- 论文中有提到单位时间内产生学习子句率高的分支策略要比低的好。
标签：Branching,
CHB,
Weighted,
变量,
Heuristic,
得分,
冲突,
multiplier,
策略
From： https://www.cnblogs.com/daweiguo/p/18587366