SampleCount version 1.0 Cornell University, 2007 April 9, 2007 See publication 'From Sampling to Model Counting' in IJCAI-07 for a detailed description of SampleCount. Briefly, SampleCount is a randomized algorithm for obtaining lower bounds on the solution counts of propositional SAT formulas. It uses sampling (through SampleSat) to identify balanced variables and variable pairs, and uses them to simplify the formula iteratively. The code is built upon the code of Approxcount version 1.2 (Wei and Selman, 2005), and uses Cachet version 1.2 (Sang et. al, 2004-2005) to compute the residual count after sufficiently many variables have been set. COMPILATION: samplecount.sh : main executable shell script; uses approxcount and cachet approxcount : type "make" in the main directory; creates version 1.2L with lowerbound computation, equivalence testing, etc. cachet : version 1.2 binary included The main executable is the script samplecount.sh, although it often helps to first experiment directly with "approxcount -lowerbound ..." using variations of the default options suggested below. The exact command line for approxcount used by samplecount.sh is printed out when executing samplecount.sh. Without any parameters, samplecount.sh reports its usage. USAGE: samplecount.sh [options for approxcount] To obtain a correctness confidence of, say, 99%, the product of and should be at least 7. It is often convenient to have 7, 4, or 2 iterations with slack being 1, 1.75, or 3.5, respectively. The exact tradeoff is discussed in the publication mentioned above. The number of samples can be around 20 on the low side to around 100 on the high. More samples generally gives more stable bounds over different iterations, but consume more time. The default options for approxcount are: -lowerbound -equiv -knuth -exact_count -100 Note that the options for Approxcount include options to SampleSat/Walksat for sampling, and will often need to be set based on the domain in order to obtain good performance. See approxcount -h for various parameter tuning options. To simply print the samples generated by SampleSat and exit, use: approxcount -sampleonly -samples N [other-options] One of the key parameter that needs adjustment is -cutoff, set by default to 10,000. It determines the number of "flips" used by SampleSat to sample each solution using Walksat. The more the flips, the longer it takes to sample but the better the sample quality (i.e., uniformity). For hard instances, the cutoff should be increased so that approxcount is able to find the requested number of samples. This can be judged by running "approxcount -lowerbound ..." directly rather than samplecount.sh on the formula and looking for the number of successful tries reported by approxcount. Another useful parameter is -noise, set by default to 50 (out of 100). Finally, -exact_time_limit determines how much time is given to Cachet to compute the exact count on the residual formula before starting the simplification process again; the default is 100 seconds. USAGE EXAMPLES: samplecount.sh example.cnf 2 20 3.5 -cutoff 5000 approxcount -lowerbound -equiv -knuth -exact_count -150 \ -samples 40 -lb_slack 3.5 -cutoff 8000 --- Please report bugs and send comments/questions to Ashish Sabharwal, sabhar at cs dot cornell dot edu.