In an influential article Papadimitriou [FOCS 1991] proved that a local search algorithm called WalkSAT finds a satisfying assignment of a satisfiable 2-CNF with $n$ variables in $O(n^2)$ expected time. Variants of the WalkSAT algorithm have become a mainstay of practical SAT solving (e.g., [Hoos and St\"utzle 2000]). In the present article we analyse the expected running time of WalkSAT on random 2-SAT instances. Answering a question raised by Alekhnovich and Ben-Sasson [SICOMP 2007], we show that WalkSAT runs in linear expected time for all clause/variable densities up to the random 2-SAT satisfiability threshold.
翻译:在一篇颇具影响力的文章中,Papadimitriou [FOCS 1991] 证明了名为WalkSAT的局部搜索算法能在$O(n^2)$的期望时间内找到包含$n$个变量的可满足2-CNF公式的一个可满足赋值。WalkSAT算法的变体已成为实际SAT求解的主流方法之一(例如[Hoos和Stützle 2000])。本文分析了WalkSAT在随机2-SAT实例上的期望运行时间。针对Alekhnovich和Ben-Sasson [SICOMP 2007]提出的问题,我们证明在子句/变量密度达到随机2-SAT可满足性阈值之前的所有情况下,WalkSAT均具有线性期望运行时间。