Walksat Home Page Stochastic Local Search for Satisfiability Bart Selman, Cornell University Henry Kautz, University of Rochester

Walksat

Version 57 - 29 Nov 2023

• Compiles under Linux, Apple OS X (Macintosh), Ansi Unix, and all versions of Microsoft Windows
• GitLab repository: https://gitlab.com/HenryKautz/Walksat

walksat.cpp for CryptoMiniSat - 1 April 2019

• Mate Soos ported the walksat code to true C++, simplified, and exhaustively debugged as part of the SAT solver CryptoMiniSat.
• This version does not include all of the flip options of version 55 and later.
• Download from https://github.com/msoos/cryptominisat

GSAT

• Before Walksat came GSAT.  Here's the original GSAT source.  It should work, but is no longer being updated.

Download GSAT source distribution

MaxWalkSat

• A version of walksat for weighted maxsat.

Download MaxWalkSat source distribution

Papers

Bart Selman, Henry Kautz, and Bram Cohen. Noise Strategies for Improving Local Search. 12th National Conference on Artificial Intelligence (AAAI-94), Seattle, WA, 1994.

Bart Selman, Henry Kautz, and Bram Cohen. Local Search Strategies for Satisfiability Testing" Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, October 11-13, 1993. David S. Johnson and Michael A. Trick, ed. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 26, AMS, 1996. Appendix summarizing results of walksat on challenge instances.

Novelty and rnovelty heuristics: David McAllester, Bart Selman, and Henry Kautz (1997). Evidence for Invariants in Local Search. 14th Conference on Artificial Intelligence (AAAI-97), Providence, RI, 1997.

Plus option for novelty heuristics: Holger H. Hoos, On the Run-time Behaviour of Stochastic Local Search Algorithms for SAT. Proceedings AAAI-99, Orlando, FL, 1999.

Adaptive cutoff option: Holger H. Hoos, An Adaptive Noise Mechanism for WalkSAT. Proceedings AAAI-2002, Edmonton, Alberta, Canada, 2002.

Home page for Bart Selman

SATLIB

SAT Live!