walksat's Introduction
Walksat - Version 56 https://gitlab.com/HenryKautz/Walksat May 2018 Please email bug reports to Henry Kautz <[email protected]> Compilation Just type: make Compilation options: make install # compile and copy to $USER/bin make clean # delete binaries For Windows Visual Studio, create a workspace/project and add the library Winmm.lib to the "linker" tab. /* Platform dependent differences: */ /* -arc4 only available on BSD and OSX. Option uses slower but */ /* stronger random number generation arc4random and */ /* arc4random_uniform */ /* WINDOWS and POSIX use rand() instead of random() */ /* Clock ticks per second determined by sysconf(_SC_CLK_TCK) */ /* for BSD, OSX, and LINUX */ /* Clock ticks per second fixed at 1000 for Windows */ /* Clock ticks per second fixed at 1 for POSIX */ Walksat Specification Walksat attempts to find a satisfying model of a conjective normal form formula. Input is cnf format: c Optional comments at start of file. c The "p" line specifies cnf format, number vars, number clauses c Variables are numbered starting at 1 c Each clause ends with 0 p cnf 3 2 1 -3 0 2 3 -1 0 Walksat reads from standard in or from a file specified as a command line argument and writes to standard out and standard error. To get a list of command line options, type walksat -help or any illegal option. ***************************************************************** Also included in distribution: makewff [-seed N] [-cnf] [-f] [-kf] clen nvars nclauses Generate random formulas using the fixed clause length model. The -seed argument can be used to initialize the random number generator. The -cnf, -f, and -kf options specify the format of the wff file; for walksat use -cnf. Clen is the length of each clause, nvars the number of variables, and nclauses the number of clauses. makequeens N Generate a N-queens formula. generate-wffs.sh Generate a numbered sequence of random 3-CNF formulas. Use: generate-wffs.sh number_vars ratio start_wff_numer end_wff_number Enter ratio as a percentage, e.g. 425 == 4.25 clause/variable. generate-hard-wffs.sh Use: generate-hard-wffs.sh number_vars start_wff_numer end_wff_number Same as generate-wffs.sh, but with ratio fixed at 4.25. ***************************************************************** Walksat: Bart Selman, Henry A. Kautz, and Bram Cohen. Noise Strategies for Improving Local Search. Proceedings AAAI-94, Seattle, WA, 1994. Novelty heuristics: David McAllester, Bart Selman, and Henry Kautz. Evidence for Invariants in Local Search. Proceedings 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. ***************************************************************** HISTORY OF MAJOR RELEASES version 07 - introduced breakcount[] array version 14 - added -super option version 16 - improved print options and help message version 17 - added trace N option version 25 - -hamming option version 28 - novelty and rnovelty heuristics version 41 - use long long ints for cutoff version 44 - special version for sat competition - not distributed version 45 - watched literals rule added version 48 - allow cnf file name to appear as argument on command line version 49 - various minor bugs, watched literals rule removed version 50 - code optimizations suggested by Don Knuth version 53 - added -plus option for -novelty and -rnovelty fixed -tabu; added heuristic -alternate; added heuristic -bigflip; added -adaptive noise option; added -nofreebie option; added -maxfreebie option; added -walkprob R to substitute for -noise N M option; replaced macro functions with inline functions; added directory of Papers to distribution; allow K and M as suffixes for -cutoff; moved distribution to gitlab.com version 54 - allocates all data structures dynamically version 55 - include -arc4 to use arc4random random number generator. version 56 - updated preprocessor #defines
walksat's People
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. ๐๐๐
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google โค๏ธ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.