An Efficient Implementation for 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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Adapting Stochastic Search For Real-time Dynamic Weighted Constraint Satisfaction
This work presents two new algorithms for performing constraint satisfaction. The first algorithm presented, DMaxWalkSat, is a constraint solver specialized for solving dynamic, weighted constraint satisfaction problems.…
A novel approach of solving the CNF-SAT problem
In this paper, we discussed CNF-SAT problem (NP-Complete problem) and analysis two solutions that can solve the problem, the PL-Resolution algorithm and the WalkSAT algorithm. PL-Resolution is a sound and complete algori…
A Probabilistic Approach to Satisfiability of Propositional Logic Formulae
We propose a version of WalkSAT algorithm, named as BetaWalkSAT. This method uses probabilistic reasoning for biasing the starting state of the local search algorithm. Beta distribution is used to model the belief over b…
Learning Interpretable Heuristics for WalkSAT
Local search algorithms are well-known methods for solving large, hard instances of the satisfiability problem (SAT). The performance of these algorithms crucially depends on heuristics for setting noise parameters and s…
reinforcement-learningAdvancing Stochastic 3-SAT Solvers by Dissipating Oversatisfied Constraints
We introduce and benchmark a stochastic local search heuristic for the NP-complete satisfiability problem 3-SAT that drastically outperforms existing solvers in the notoriously difficult realm of critically hard instance…