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 数的下界的猜想。

局部搜索的线性权重转移规则

A Linear Weight Transfer Rule for Local Search

MD4 and MD5 are seminal cryptographic hash functions proposed in early 1990s.
MD4 consists of 48 steps and produces a 128-bit hash given a message of
arbitrary finite size. MD5 is a more secure 64-step extension of MD4. Both MD4
and MD5 are vulnerable to practical collision attacks, yet it is still not
realistic to invert them, i.e. to find a message given a hash. In 2007, the
39-step version of MD4 was inverted via reducing to SAT and applying a CDCL
solver along with the so-called Dobbertin's constraints. As for MD5, in 2012
its 28-step version was inverted via a CDCL solver for one specified hash
without adding any additional constraints. In this study, Cube-and-Conquer (a
combination of CDCL and lookahead) is applied to invert step-reduced versions
of MD4 and MD5. For this purpose, two algorithms are proposed. The first one
generates inversion problems for MD4 by gradually modifying the Dobbertin's
constraints. The second algorithm tries the cubing phase of Cube-and-Conquer
with different cutoff thresholds to find the one with minimal runtime
estimation of the conquer phase. This algorithm operates in two modes: (i)
estimating the hardness of an arbitrary given formula; (ii) incomplete
SAT-solving of a given satisfiable formula. While the first algorithm is
focused on inverting step-reduced MD4, the second one is not area-specific and
so is applicable to a variety of classes of hard SAT instances. In this study,
for the first time in history, 40-, 41-, 42-, and 43-step MD4 are inverted via
the first algorithm and the estimating mode of the second algorithm. 28-step
MD5 is inverted for four hashes via the incomplete SAT-solving mode of the
second algorithm. For three hashes out of them this is done for the first time.

该研究利用 CDCL 和 Cube-and-Conquer 算法结合，提出两种算法来反演 MD4 和 MD5 的步长降低版本，并对 40~43 步 MD4 和 28 步 MD5 进行了反演。