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.

本文提出对固定权重算法（ddfw）进行三个修改：动态权重转移方法，在局部最小值的子句之间移动权重；调整如何在局部最小值中选择满意的子句，以获得权重；加权随机选择变量翻转方法。在多个基准测试中，我们验证了我们对 ddfw 的改进，在硬组合实例方面表现良好，并以改进的求解器独家解决了 Ahmed 等人 (2014) 提出的两个 Van der Waerden 数的下界的猜想。