The Divide and Distribute Fixed Weights algorithm (ddfw) is a dynamic local search SAT-solving algorithm that transfers weight from satisfied to falsified clauses in local minima. ddfw is remarkably effective on several hard combinatorial instances. Yet, despite its success, it has received little study since its debut in 2005. In this paper, we propose three modifications to the base algorithm: a linear weight transfer method that moves a dynamic amount of weight between clauses in local minima, an adjustment to how satisfied clauses are chosen in local minima to give weight, and a weighted-random method of selecting variables to flip. We implemented our modifications to ddfw on top of the solver yalsat. Our experiments show that our modifications boost the performance compared to the original ddfw algorithm on multiple benchmarks, including those from the past three years of SAT competitions. Moreover, our improved solver exclusively solves hard combinatorial instances that refute a conjecture on the lower bound of two Van der Waerden numbers set forth by Ahmed et al. (2014), and it performs well on a hard graph-coloring instance that has been open for over three decades.

翻译：划分与分配固定权值算法（Divide and Distribute Fixed Weights，简称ddfw）是一种动态局部搜索SAT求解算法，该算法在局部最优状态下将权值从满足子句转移至未满足子句。ddfw在多个困难的组合实例上表现出显著有效性。然而，尽管其成果斐然，自2005年首次提出以来，该算法鲜少受到深入研究。本文针对基础算法提出三项改进：一种线性权值转移方法，可在局部最优状态下在子句间动态移动权值；一种调整局部最优状态下选择提供权值的满足子句的方式；以及一种加权随机选取变量翻转的方法。我们在求解器yalsat基础上实现了对ddfw的改进。实验表明，与原始ddfw算法相比，我们的改进在多个基准测试（包括过去三年SAT竞赛中的测试集）上提升了性能。此外，改进后的求解器能独家解决一些困难的组合实例，这些实例驳斥了Ahmed等人（2014年）关于两个范德瓦尔登数下界的猜想，并在一个已公开三十余年的困难图着色实例上表现优异。