- Optimized BCP:
我们说一个子句是隐含的，如果它的所有文字（只有一个）都被赋值为零。因此，为了有效地实现BCP，我们希望找到一种方法来快速访问通过一组赋值的单个添加而新隐含的所有子句。
最直观的方法是简单地查看数据库子句中包含当前赋值设置为0的文字的每个子句。实际上，我们将为每个子句保留一个计数器，以指示子句中有多少值为0的文字，并在每次将子句中的文字设置为0时修改计数器。但是，如果子句有N个文字，那么当1、2、3、4、…、N-1个文字设置为零时，我们就不需要访问它。我们只想在“零文字数”计数器从N-2变为N-1时访问它。
在每个子句中选择任意两个未分配给0的文字进行观察。因此，我们可以保证，在这两个文字中的一个被赋值为0之前，子句中被赋值为零的文字不能超过N-2个，也就是说，子句不是隐含的。现在，我们只需要在两个被关注的文字中的一个被赋值为零时访问每个子句。当我们访问每个子句时，必须满足以下两个条件之一：
（1）子句不是隐含的，因此至少有2个文字没有赋值为零，包括当前关注的另一个文字。这意味着至少有一个未被关注的文字未被赋值为零。我们选择这个文字来替换刚刚分配给零的文字。因此，我们保留了两个被关注的文字不分配给0的特性。
（2） 该子句是隐含的。遵循访问隐含子句的程序（通常，这会产生新的隐含，除非该子句已经被sat）。应该注意的是，隐含变量必须始终是另一个受关注的文字，因为根据定义，子句只有一个文字没有赋值为零，而两个受关注文字中的一个现在被赋值为零。
双文本观察方案的一个关键好处是，在回溯时，不需要修改子句数据库中的观察文本。因此，取消变量赋值可以在常数时间内完成。此外，重新赋值最近赋值过被取消赋值的变量往往比第一次赋值更快。这大大减少了内存访问的总数，而数据缓存未命中率高是大多数SAT实现的主要瓶颈。 - Variable State Independent Decaying Sum (VSIDS) Decision Heuristic
（1）每个变量的正负极性都有一个计数器，初始化为 0
（2）将子句添加到数据库中时，子句中的每个文字关联的计数器将递增。
（3）每次决策时都会选择计数器最高的（未赋值的）变量和极性。
（4）默认情况下，平局是使用随机策略，这是可配置的
（5）定期地，所有计数器除以常数
总的来说，这种策略可以被视为试图满足冲突子句，但特别是试图满足最近的冲突子句。
当然，这种策略的另一个关键特性是，由于它与变量状态无关（除非我们必须选择一个未赋值的变量），它的开销非常低，因为只有在发生冲突时才会更新统计数据，相应地，还会更新新的冲突子句。即便如此，在一些困难的实例中，与决策相关的计算仍占运行时间的约10%。（冲突分析也占运行时间的约10%，其余约80%的时间用于BCP。）最终，采用这种策略显著地（即一个数量级）提高了所有最困难问题的性能，而不会损害任何更简单问题的性能。 - Other Features
4.1 子句删除
Chaff 使用定时惰性子句删除。当添加每个子句时，都会对其进行检查，以确定在未来的什么时候（如果有的话）应该删除该子句。所使用的度量是相关性，因此当子句中超过N个（其中N通常为100-200）的文字首次变为未赋值时，该子句将被标记为已删除。与已删除子句相关联的实际内存是通过不常见的单片数据库压缩来恢复的。
4.2 重启
重新启动包括清除所有变量（包括所有决策）的状态，然后正常进行。重启之前的学习子句仍然保留，因此求解器不会再重复之前的分析。此外，可以添加一定量的随机性到决策过程中，以帮助选择新的搜索路径。这种随机性通常很小，并且只持续几个决策。
应该注意的是，重新启动会影响算法的完备性。然而，如果保留所有子句，则算法仍然是完整的，因此可以通过随着时间缓慢增加相关性参数N来保持完备性。GRASP使用类似的策略，通过每次重新启动都延长重新启动周期来保持完备性（Chaff在默认情况下也会这样做，因为它通常会提高性能）。
Chaff的重新启动与GRASP等使用的重新启动不同，因为它们不会影响当前的决策统计信息。它们主要是为了提供一个机会，根据当前的问题状态更改早期决策，包括所有添加的子句和当前的搜索路径。在默认设置下，Chaff可以在 hard 实例（sat或unsat）上重新启动数千次，尽管在完全禁用重新启动的情况下通常（或至少有时）可以获得类似的结果。 - 实验结果
在运行时间相对不重要的较小示例中，Chaff可与任何其他求解器相媲美。然而，在其他解算器挣扎或放弃的更大例子中，Chaff通过比最好的公共领域解算器少一到两个数量级的时间完成而占据主导地位。
Chaff: Engineering an Efficient SAT Solver——2001
©著作权归作者所有,转载或内容合作请联系作者
- 文/潘晓璐 我一进店门，熙熙楼的掌柜王于贵愁眉苦脸地迎上来，“玉大人，你说我怎么就摊上这事。” “怎么了？”我有些...
- 文/花漫 我一把揭开白布。 她就那样静静地躺着，像睡着了一般。 火红的嫁衣衬着肌肤如雪。 梳的纹丝不乱的头发上，一...
- 文/苍兰香墨 我猛地睁开眼，长吁一口气：“原来是场噩梦啊……” “哼！你这毒妇竟也来了？” 一声冷哼从身侧响起，我...
推荐阅读更多精彩内容
- Go 语言实战: 编写可维护 Go 语言代码建议 目录 1. 指导原则1.1 简单性1.2 可读性1.3 生产力...
- 基础议题：指针、引用、类型转换、arrays、constructors 条款1：仔细区分指针和引用 引用在某种程度...
