Authors: Wei Wei and Bart Selman
See details in paper: A New Approach to Model Counting, SAT-07, June 2005

-------------------

bart: modified to print out sampled solutions. done in "save_solution" routine.

type "make" in current directory, and the program should compile.
run the program by

./approxcount <yourcnf.cnf

-seed N
-cutoff N
-tries N number of tries taken at each step
-samples N number of samples (successful tries) taken at each step
-sa SA_RATIO TEMPERATURE walksat with SA_RATIO percent SA
               moves added at temp TEMPERAURE/100. (default: -sa 50 10)
-noise N or -noise N M (default M = 100)
-dont_care_fract N   consider variables that are positive in 
               (50-N)%c to (50+N)%c samples to be dont_cares,
               and set the multiplier to be 2. (default N = 0)
-exact_count N   start exact count from the Nth iteration (default N = 50
to disable exact count, use -exact_count 0\n");
to start exact count when N variables remain, use -exact_count -N
-exact_time_limit N  try exact count for N seconds in each iteration (defualt N = 100)
-verify  use cachet to veify the accuracy of multipliers
-doublecheck  use both cachet and relsat to count the sulutions exactly
-inclnonsoln  include non-solution states in sampling counts
-early_sa  use mixed simulated annealing moves from the start of search
-nounitprop do not use unitpropagation
-pickuneven  branch on the most unevenly sampled variable (default)
-pickeven  branch on the most evenly sampled variable
-pickrand  branch on a random variable
-pickuneven  branch on the lowest numbered variable
-imbalance N  choose pickrandom, and assert a literal only if (50+N)%c 
               of the sample agree with the assertion (default: N = 0)
if more than one of the above 6 options selected, only the last one is effective