An Efficient Implementation for WalkSAT
This work provides an incremental improvement to a widely used stochastic local search algorithm for SAT, benefiting researchers and practitioners in computational logic and AI.
The authors tackled the problem of improving the efficiency of the WalkSAT algorithm for solving Boolean satisfiability (SAT) by reducing redundant calculations, resulting in a dramatically faster implementation that outperforms the latest versions and variants of WalkSAT.
Stochastic local search (SLS) algorithms have exhibited great effectiveness in finding models of random instances of the Boolean satisfiability problem (SAT). As one of the most widely known and used SLS algorithm, WalkSAT plays a key role in the evolutions of SLS for SAT, and also hold state-of-the-art performance on random instances. This work proposes a novel implementation for WalkSAT which decreases the redundant calculations leading to a dramatically speeding up, thus dominates the latest version of WalkSAT including its advanced variants.