************************** 
Software: Backbone Guided WalkSAT for SAT and Max-SAT with Dynamic
Noise Ratio

Moshe Looks, Ananda Rangan and Weixiong Zhang
Department of Computer Science and Department of Genetics
Washington University in St. Louis, St. Louis, MO 63130, USA
email:  moshelooks@yahho.com, zhang@cse.wustl.edu

01/26/2002 - 9/10/2003

**************************

(Introduction you see on the webpage:)

Here is the package of programs we developed for the backbone guided
WalkSAT algorithm with dynamic noise ratio for SAT and Max-SAT.  Our
software was built on top of the WalkSAT local search algorithm and
software (downloaded from Henry Kautz's homepage).  The original idea
of the dynamic noise ratio method was due to Holger Hoos.  We
implemented (after some struggling effort) and tested it on 3-SAT and
Max-3-SAT.  To learn more about the backbone guided local search
method with dynamic noise ratio, take a look at a paper presented at
IJCAI-03.

The package can be downloaded here (gzipped tar file). Use "tar -xzf
filename" to unzip the package.  See the README file for details on
installation and usage.  We used a Linux box for the development and
test.

Note: The README file should be sufficient for a quick installation
and use of the software.  We cannot guarantee any support.

**************************

*** Note: This package was developed by two people, one on the backbone
guilded WalkSAT and the other on using a dynamic noise ratio later.
Below, we describe how to use the dynamic noise ratio first, and then
the installation and the usage of the backbone guided search.

**************************
To use dynamic noise, add the command line option

-adaptive phi_numerator theta_numerator
The noise setting now becomes the initial noise level, and we set:
phi=phi_numerator/denominator theta=theta_numerator/denominator
where denominator is the second arg to noise.

-longrun X, when used in conjunction with the -learn option, changes the
number of flips allowed for runs after the learning phase to X.  So for
example,

bgwalksat -cutoff 20000 -tries 37 -learn 30 1 -longrun 200000
will to 30 runs with 20,000 flips each (the learning phase), followed by 7
runs with 200,000 flips each (the pseudobackbone-phase), for a total of
2,000,000 flips.

BTW, avoid the makewff utility, it is messed up.  I recommend writing your
own random fomula generator, so you know exactly what you are getting; should
take only a few minutes...  

**************************
--- How to get started ?

Use make to build move the built programs and all the files in the
script files to a general lib directory.  Update the PATH to this lib
directory.  This completes the installation.

--- How to use bgwalksat program?

bgwalksat program options
----------------------------
bgwalksat -h will give a set of options as follows

General parameters:
  -seed N -cutoff N -restart N
  -numsol N = stop after finding N solutions
  -super = use the Luby series for the cutoff values
  -init FILE = set vars not included in FILE to false
  -partial FILE = set vars not included in FILE randomly
  -status = return fail status if solution not found
  -target N = succeed if N or fewer clauses unsatisfied

Heuristics:
  -random -best -tabu N -novelty -rnovelty
  -novelty+ RN RM = modify novelty by RN/RM random walk
  -learn <learn start> <learn step>  use this option to enable back bone learning
  -bestvar = uses bestvariable pick strategy instead of greedy pick strategy
  -bkbpick- uses back bone pick instead of random pick strategy
  -bkbinit- uses back bone probabilities for initialization
  -cbkpick - biased clause pick
  -zbrkpick - biased zero breakcount pick
  -noise N or -noise N M (default M = 100)

// description of options
// -learn <say 30> <say 5>  should be specified for the following options to work
// -bestvar option if specified turns ON Biased Greedy Pick
// -bkbpick option if specified turns ON Biased Noisy Pick
// -cbkpick option if specified turns ON Biased Clause Pick using clause backbone
// -zbrkpick option if specified turns ON Biased zero break count pick
// -bkbinit option  if specified turns ON Biased assignment generation
// if none of these are turned ON then -best -novelty etc. options are looked for
// the program takes -best heuristic as default which is nothing but WalkSAT-SKC

Printing:
  -out FILE = print solution as a list of literals to FILE
  -extfile  FILE = print local minimas to FILE for analysis
  -trace N = print statistics every N flips
  -assign N = print assignments at flip N, 2N, ...
  -sol = print satisfying assignments to stdout
  -solcnf = print sat assign to stdout in DIMACS format, and exit
  -low = print lowest assignment each try
  -bad = print unsat clauses each try
  -hist = print histogram of tail
  -tail N = assume tail begins at nvars*N
  -sample N = sample noise level every N flips
  -anytime  prints anytime information
  -printstat  prints .raw output .cost .0cost and .time outputs

// description
// -extfile <fn>  should be specified to get all the following diagnostic information
// using -printstat  .raw .cost and .0cost files are printed out
// .raw file contains all the raw data which can be further processed to get the
// actual data
// -anytime prints a .anytime information file

Example usage :
 makewff -seed $i  -cnf  3 2000 8600 > temp2.cnf
 bgwalksat -seed $i -noise $j -best  -restart 100  -cutoff 10000  -out output -extfile exp1_wlksat_$j -printstat    < temp2.cnf  


$i and $j are script parameters.

Now to turn ON biased noisy pick with backbone learning .. learning threshold 30 learning step 5

 bgwalksat -seed $i -noise $j -learn 30 5 -bkbpick  -restart 100  -cutoff 10000  -out output -extfile exp1_wlksat_$j -printstat    < temp2.cnf  


How to collect statistics?

specify the -printstat option and specify the extension file name -extfile <fn>

Here I describe one of the script files and explain how it works.
I also describe the avgcalc program which is used by the script files makesummary*
to compare various heuristics.

==============================================================================
i=0
while [  "$i"  -lt  200   ]
do

j=10
while [ "$j"   -lt  110 ]
do
 makewff -seed $i  -cnf  3 2000 8600 > temp2.cnf

 bgwalksat -seed $i -noise $j -best  -restart 100  -cutoff 10000  -out output -extfile exp1_wlksat_$j -printstat    < temp2.cnf  

 bgwalksat -seed $i -noise $j -restart 100  -cutoff 10000  -out output -extfile exp1_cbkpick_$j  -learn 30 5 -cbkpick -weight 1 -printstat   < temp2.cnf  

 bgwalksat -seed $i -noise $j -restart 100  -cutoff 10000  -out output -extfile exp1_bkinit_$j    -learn 30 5 -bkbinit -weight 1 -printstat < temp2.cnf 

 j=`expr $j + 10`
done

 i=`expr $i + 1` 
done
=============================================================================

Use the makesummary_cbkpick script (shown below) to compare .raw files and 
print the cbkpick_summary.avg file which gives the cost difference with
95 percent confidence interval between walksat and biased clause pick 
strategy.

avgcalc takes two columns of numbers(specified -col1 and -col2) from two different files specified by -in1 and -in2
options. Prints the comparison data to cbkpick_summary.* files. -printthis option is used
to print a number at the start of the analyzed data to indicate the noise ratio.
The file cbkpick_summary.avg is ready to be plotted as a graph. 

avgcalc -in1 exp1_wlksat_10.raw  -in2  exp1_cbkpick_10.raw -col1 3 -col2 3 -out cbkpick_summary -printthis 10
avgcalc -in1 exp1_wlksat_20.raw  -in2  exp1_cbkpick_20.raw -col1 3 -col2 3 -out cbkpick_summary -printthis 20
avgcalc -in1 exp1_wlksat_30.raw  -in2  exp1_cbkpick_30.raw -col1 3 -col2 3 -out cbkpick_summary -printthis 30
avgcalc -in1 exp1_wlksat_40.raw  -in2  exp1_cbkpick_40.raw -col1 3 -col2 3 -out cbkpick_summary -printthis 40
avgcalc -in1 exp1_wlksat_50.raw  -in2  exp1_cbkpick_50.raw -col1 3 -col2 3 -out cbkpick_summary -printthis 50
avgcalc -in1 exp1_wlksat_60.raw  -in2  exp1_cbkpick_60.raw -col1 3 -col2 3 -out cbkpick_summary -printthis 60
avgcalc -in1 exp1_wlksat_70.raw  -in2  exp1_cbkpick_70.raw -col1 3 -col2 3 -out cbkpick_summary -printthis 70
avgcalc -in1 exp1_wlksat_80.raw  -in2  exp1_cbkpick_80.raw -col1 3 -col2 3 -out cbkpick_summary -printthis 80
avgcalc -in1 exp1_wlksat_90.raw  -in2  exp1_cbkpick_90.raw -col1 3 -col2 3 -out cbkpick_summary -printthis 90
avgcalc -in1 exp1_wlksat_100.raw  -in2  exp1_cbkpick_100.raw -col1 3 -col2 3 -out cbkpick_summary -printthis 100


How to turn on various heuristics ?

Various heuristics can be turned ON by specifying the appropriate flag for the heuristic. 
bgwalksat -h gives the info on options available.


What are the script files?

a)Script files to compare different heuristics on random problem instances.

 makesummary          makesummary_bkinit  makesummary_both     makesummary_zbrkpick  
 makesummary_bestvar  makesummary_bkpick  makesummary_cbkpick

These script files are similar to the one explained before.

b) Script files to test real problem instances.

testall is the script file (shown below) The filename specified by $2
collects all the data printed by bgwalksat.

the makegraph_data extracts the relevant information from $2 and 
prepares $2.graph which gives the success rate information 

-----------------------------------------------------------------------------------------
j=0
while [ "$j"   -lt  102 ]
do
i=1
while [  "$i"  -lt  11   ]
do
 bgwalksat -cbkpick -bkbpick -bestvar -bkbinit -tries 100 -noise $j -cutoff 100000 -learn 30 5 < $1 >> $2
 i=`expr $i + 1` 
done
j=`expr $j + 10`
done
makegraph_data $2 $2.graph
--------------------------------------------------------------------------------------------