SAT Instance Statistical Analysis Kit
by Wenjie Fang

This is a quick-and-dirty written kit for SAT instance statistical analysis. It contains a C program for analysing SAT instances, a quick-hacked on an implementation of KMeans++ clustering algorithm (from http://www.stanford.edu/~darthur/kmpp.zip), and a Perl script to glue this two parts together.

To use it, copy every file under directory kit to a directory full of SAT instances in CNF format, then run the perl script analysedir.pl. The whole analysis takes several steps: 

1. It checks if a SAT instance analysis has been done before. If such analysis does not exists, it will find recursively every .CNF file under current directory and use the program "analyse" to obtain statistics from these SAT instances. This step takes a long time for industrial instances. 

2. It asks you what features you would like to keep in the clustering step. If there is a previously chosen feature file, you may also choose to use features previously chosen.

3. Due to the nature of KMeans-alike algorithm, it cannot predict how many clusters there are in the file. Therefore, it will ask you for an estimation of number of clusters. Finally, it will format data files for KMeans++ clustering, then executes KMeanspp to do clustering. The result file is clustered_stats.txt.

4. It cleans up temporary files.

Here follows a description of files that may be present during analysis.

***** Files in the kit *****

* analysedir.pl

Perl script that glues the statistic part and the clustering part together. The script to run for automatic analysis and clustering. For more details about this process, please have a look at the script analysedir.pl. It is in plain Perl, with some comments on the side, therefore it should not be too hard to understand.

* analyse

Main program for extracting statistics from SAT instances.

* KMeanspp

Main program for k-means++ clustering. This is a quick hack on the implementation of k-means++ by David Arthur. The original source code can be found at http://www.stanford.edu/~darthur/kmpp.zip. Its (modified) source code is also provided in kmpp.tar.gz.

* features.txt

Text file containing all statistical features provided by the program analyse. It is used in analysedir.pl for interactive feature selection, but it can also be regarded as a readable list explaining features provided by the program analyse.

* sat_input_template.txt

Template input file for KMeanspp. Indicates the algorithm used in the clustering, restart times, etc. For more information, please have a look at the README file in the original source code. Normally, there is no need to modify this file.

***** Source code *****

* analyse.c

Source code of the program analyse. If you would like to know more details about how this program functions, please read this source code file. It is in plain C, no fancy code nor obfuscated code, and it contains enough (I hope so) comments to make the code even clearer.

* kmpp.tar.gz

A tarball containing source code of KMeanspp. Original source code of David Arthur's k-means++ implementation can be found at ttp://www.stanford.edu/~darthur/kmpp.zip.

***** Files as result of analysis *****

* inventory.txt

Contains name of every SAT instance in CNF format analysed.

* toobig.txt

Contains name of SAT instance that the program analyse fails to analyse. This is generally caused by extremely large industrial instances. Even reading them in memory may cause the program to crash due to insufficient memory. They are discarded in both inventory.txt and stats.txt.

* stats.txt

Contains statistics of every SAT instance in CNF format analysed, with respect to order in inventory.txt.

* clustered_stats.txt

Contains selected statistics and clustering result of every SAT instance in CNF format analysed, with respect to order in inventory.txt. Clustering result for each instance is in the last column.

* features_chosen.txt

Contains selected features in numeric form.

* features_chosen_readable.txt

A human readable version of features_chosen.txt.

***** Temporary files (get deleted once analysis is finished) *****

* invtmp.txt

Temporary version of inventory.txt, with instances that fail to be analysed.

* statstmp.txt

Temporary version of stats.txt, in which empty lines means instances that fail to be analysed.

* pstats.txt

Temporary file storing selected statistics of SAT instances.

* pstats_c.txt

A decorated version of pstats.txt for KMeanspp.

* sat_input.txt

Temporary input file for KMeanspp copied from sat_input_template.txt, with cluster number indication.

* res.kmpp.kmpp.kmpp.txt

Result of clustering provided by KMeanspp. This strange file name is an evidence that this hack is really dirty.
