Walksat
GSAT and WalkSat are local search algorithms to solve Boolean satisfiability problems. Both algorithms work on formulae that are in, or have been converted into, conjunctive normal form. They start by assigning a random value to each variable. If the assignment satisfies all clauses, the algorithm terminates, returning the assignment. Otherwise, a variable is flipped and the above is then repeated until all the clauses are satisfied. WalkSAT and GSAT differ in the methods used to select which variable to flip. GSAT makes the change which minimizes the number of unsatisfied clauses in the new assignment, or with some probability picks a variable at random. WalkSAT first picks a clause which is unsatisfied by the current assignment, then flips a variable within that clause. The clause is generally picked at random among unsatisfied clauses. The variable is generally picked that will result in the fewest previously satisfied clauses becoming unsatisfied, with some probability of picking one of the variables at random. When picking at random, WalkSAT is guaranteed at least a chance of one out of the number of variables in the clause of fixing a currently incorrect assignment. When picking a guessed to be optimal variable, WalkSAT has to do less calculation than GSAT because it’s considering fewer possibilities.
(Source: http://en.wikipedia.org/wiki/WalkSAT)
Keywords for this software
References in zbMATH (referenced in 184 articles )
Showing results 1 to 20 of 184.
Sorted by year (- Paes, Aline; Zaverucha, Gerson; Costa, Vítor Santos: On the use of stochastic local search techniques to revise first-order logic theories from examples (2017)
- Bischl, Bernd; Kerschke, Pascal; Kotthoff, Lars; Lindauer, Marius; Malitsky, Yuri; Fréchette, Alexandre; Hoos, Holger; Hutter, Frank; Leyton-Brown, Kevin; Tierney, Kevin; Vanschoren, Joaquin: ASlib: a benchmark library for algorithm selection (2016)
- Gao, Jian; Wang, Jianan; Yin, Minghao: Experimental analyses on phase transitions in compiling satisfiability problems (2015) ioport
- Wagner, Glenn; Choset, Howie: Subdimensional expansion for multirobot path planning (2015)
- Wang, Jinyan; Yin, Minghao; Wu, Jingli: Approximate model counting via extension rule (2015)
- Angiulli, Fabrizio; Ben-Eliyahu-Zohary, Rachel; Fassetti, Fabio; Palopoli, Luigi: On the tractability of minimal model computation for some CNF theories (2014)
- Simmonds, Jocelyn; Ben-David, Shoham; Chechik, Marsha: Monitoring and recovery for web service applications (2013)
- Maratea, Marco: Planning as satisfiability with IPC simple preferences and action costs (2012)
- Martins, Ruben; Manquinho, Vasco; Lynce, In^es: An overview of parallel SAT solving (2012)
- Rintanen, Jussi: Planning as satisfiability: heuristics (2012)
- Sutton, Andrew M.; Whitley, L.Darrell; Howe, Adele E.: Computing the moments $k$-bounded pseudo-Boolean functions over Hamming spheres of arbitrary radius in polynomial time (2012)
- Triska, Markus; Musliu, Nysret: An improved SAT formulation for the social golfer problem (2012)
- Baioletti, Marco; Milani, Alfredo; Poggioni, Valentina; Rossi, Fabio: Experimental evaluation of pheromone models in ACOPlan (2011)
- Benoist, Thierry; Estellon, Bertrand; Gardi, Frédéric; Megel, Romain; Nouioua, Karim: LocalSolver 1.x: A black-box local-search solver for 0-1 programming (2011)
- Bienvenu, Meghyn; Fritz, Christian; Mcilraith, Sheila A.: Specifying and computing preferred plans (2011)
- Cooper, Martin C.; De Roquemaurel, Marie; Régnier, Pierre: A weighted CSP approach to cost-optimal planning (2011)
- Giunchiglia, Enrico; Maratea, Marco: Introducing preferences in planning as satisfiability (2011)
- Kroc, Lukas; Sabharwal, Ashish; Selman, Bart: Leveraging belief propagation, backtrack search, and statistics for model counting (2011)
- Mengshoel, Ole J.; Roth, Dan; Wilkins, David C.: Portfolios in stochastic local search: efficiently computing most probable explanations in Bayesian networks (2011)
- Nair, Naveen; Govindan, Anandraj; Jayaraman, Chander; Kiran, T.V.S.; Ramakrishnan, Ganesh: Pruning search space for weighted first order Horn clause satisfiability (2011)