HISTORY version 7 - introduced breakcount[] array version 11 - if all vars in a clause are tabu, pick another clause version 14 - universal sequence version 16 - improved print options and help message version 17 - added trace N option version 18 - added avg # unsat in tail version 19 - fixed bug in calc. of avg # unsat in tail version 21 - fixed help message version 22 - used POSIX times() function version 23 - calculate std dev of avgfalse in tail version 25 - -hamming option version 26 - simplified inner loop version 27 - major cleanup, reorganized distribution file version 28 - novelty and rnovelty heuristics version 30 - fixed bug in calcuation of mean restarts, and added: novelty, rnovelty, noise calculations version 31 - fix divide by 0 core dump version 32 - fix bug in tabu code version 33 - print mean flips until assign after each try. version 34 - allow numsol to work with solcnf version 35 - fixed printing of columns version 36 - adjusted formatting of output version 37 - cleaned up, Makefile for gcc, option of printing solution to a file, fixed bugs in -target option version 38 - added rnovelty+; but performance is poor on random 3 sat formulas, contrary to expectations from H. Hoos; paper; some detail of implementation may be critical! version 39 - fixed, should be novelty+, not rnovelty+. version 40 - compiles now under NT, ansi unix, as well as most other Unix's version 41 - uses long long ints for cutoff version 42 - fixed bug in rnovelty when demoninator not 100 version 43 - finally included CORRECT versions of novelty+ and rnovelty+. version 44 - special version for sat competition - not distributed version 45 - speedup by Alex Fukunaga , see below Thu Jan 15 21:13:56 PST 2004 ******************************************************************************** Compilation notes: - Edit flags at beginning of walksat.c - For Windows, create a workspace/project and add the library Winmm.lib to the "linker" tab. ******************************************************************************** Walksat specifications Walksat attempts to find a satisfying model of a generalized cnf formula. It only accepts the cnf format; e.g.: c Optional comments c at start of file. c The "p" line specifies cnf format, number vars, number clauses p cnf 3 2 1 -3 0 2 3 -1 0 Compile walksat by simply typing "make". Walksat reads from standard in and writes to standard out (and standard error). To get a list of command line options, type walksat -help (or any other illegal option). LIMITS ON WFF SIZE The constant MAXATOM limits the number of atoms; you can increase this necessary to accommodate larger problems. The limit on the number of clauses can be adjusted in two ways: either (1) change the constant MAXCLAUSE, or (2) compile with the command make dynamic The "dynamic" option causes the array of clause pointers to be dynamically allocated. This uses memory more efficiency, but the program runs somewhat slower with some compilers. ************ Also included in the distribution is a random formula generator, makewff. Use: makecnf [-seed N] [-cnf] [-f] [-kf] clen nvars nclauses 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. From: Alex Fukunaga Subject: A patch for speeding up your Walksat code To: kautz@cs.washington.edu Date: Thu, 26 Feb 2004 15:55:19 -0800 (PST) Dear Prof. Kautz, Hello, I'm a Ph.D. student at UCLA working with Rich Korf. I hope you remember me -- we met at the IJCAI workshop on stochastic search last year. I was recently working on a survey paper on implementation techniques for SAT local search, and I found an improvement to the Walksat variable flip algorithm (i.e., the flipatom() function). The search behavior (the assignments explored) is totally *unaffected* it just speeds up var flips processing. This works with all the R/Novelty/+ variants as well. I implemented this speedup in your Walksat v43 code, and found that it improves the flip rate significantly (by 30-50% for large problems), so I thought I'd send the patched code to you in case you'd like to incorporate the speedup in future releases of your Walksat code. An analysis of the speedup is in a paper submitted to SAT2004. (http://www.bol.ucla.edu/~fukunaga/sat2004-submitted.pdf) [The experimental results in the paper are based on a Lisp prototype, so timings are different than with the Walksat43-based code]. The improved flip algorithm is also an improvement over the algorithm used by UBCSAT (by Holger Hoos' student), which is the "watch-1" strategy described in the paper. In the attached code, all of my changes are enclosed with an "#ifdef_WATCH" directive, so the feature can be enabled/disabled using the _WATCH flag. I've tested the code thoroughghly, and verified that all the output (when compiled with/without the _WATCH flag enabled) is *identical* except for the runtime and the flips per second. Hope you find this useful. Regards, Alex Fukunaga UCLA Computer Science Department and JPL Artificial Intelligence Group http://www.bol.ucla.edu/~fukunaga/