WalkSAT as an Informed Heuristic to DPLL in SAT Solving

Abstract

It is well known that stochastic search methods tend to outperform systematic search approaches in solving randomly generated SAT problems. Typically, stochastic local search algorithms like GSAT and WalkSAT can solve hard, randomly generated problems that are significantly larger than those handled by traditional complete search algorithms like DPLL. However, unlike DPLL, local search algorithms are not complete and, as a consequence, cannot prove unsatisfiability. Therefore it is desirable to find a hybrid of these two approaches that leverages the strength of both. First, we present a set of initial experiments generated to find exploitable areas in DPLL and WalkSAT. Second, we propose that WalkSAT is a candidate for generating dynamic heuristics