1. Anton Belov
  2. crsat-2.0

Overview

HTTPS SSH
Usage:

crsat -tries=<tries> -cutoff=<cutoff> -wp=<noise> -timeout=<timeout> <input-file-name>


<tries>   - number of tries [int]
<cutoff>  - max steps per try [int]
<noise>   - probability of random walk [float: 0.0 ... 1.0]
<timeout> - timeout per try [int, seconds]
<input-file-name> - must be a binary AIG (i.e. .aig, but not .aag);
                    maybe GZIP compressed or not (ends with .aig or .aig.gz)


Example:

crsat -tries=100 -cutoff=10000 -wp=0.1 -timeout=300 ../benchmarks/hwmcc08-aag-sat/139442p0neg.aig.gz

Output:

# try found steps time(ms) sps jfs_init jfs_best jfs_avg jfs_best_step obj_init obj_best obj_avg obj_best_step rwalks flips props_up props_down props_side confls_up confls_down confls_side rn_state bcp_prop_deqs bcp_state_deqs
1 1 36866 500 73732 1 0 18.1 36865 1 0 18.1 36865 3620 69501 0 0 0 0 0 0 814502495 2436987 3753274 
2 1 27983 370 75629 1 0 19.2 27982 1 0 19.2 27982 2759 53185 0 0 0 0 0 0 1860725436 1836106 2811713 
...
10 1 26242 360 72894 1 0 19.1 26241 1 0 19.1 26241 2635 49858 0 0 0 0 0 0 1750663136 1662172 2590430 
# run
# succ_rate med_steps avg_steps stdev_steps stdev_avg_steps med_time avg_time stdev_time stdev_avg_time avg_steps_succ avg_time_succ avg_sps avg_init_jfs avg_best_jfs avg_jfs avg_rwalk props_p_step confls_p_step 
90.00 27515.00 34506.50 27089.32 0.79 370.00 465.00 356.04 0.77 27229.45 370.00 71612.80 1.00 0.10 19.99 3419.70 0.00 0.00 

Interpretation:

The lines after "# try" present results for each individual try; first four columns
are intepreted as: try number, SAT assignment found (1) or not (0), number of steps,
time (in milliseconds)

The lines after "# run" present statistics over all tries: med_ stands for median,
avg_ stands for average, stdev_ is standard deviation, etc.

Please email me in case of questions.

The paper that describes the solver:
A. Belov, M. Järvisalo, and Z. Stachniak. Depth-Driven Circuit-Level Stochastic Local Search for SAT. In Proceedings of IJCAI-11.
http://anton.belov-mcdowell.com/baker/media/papers/belov_jarvisalo_stachniak--ijcai11.pdf

Cheers,
Anton