cmpsat - Tool for Comparison of SAT Solvers
===============================================

This program is intended for comparison of two SAT solvers. It implements
the statistical methodology proposed by Mladen Nikolic (Faculty of
Mathematics, University of Belgrade, Serbia.)

The original program can be obtained from:

	http://www.matf.bg.ac.rs/~nikolic/solvercomparison/

The latest version of this fork can be obtained from:

	http://github.com/vegard/cmpsat

This program uses ALGLIB (http://www.alglib.net).


License
=======

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation (www.fsf.org); either version 2 of the 
License, or (at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

A copy of the GNU General Public License is available at:

	http://www.fsf.org/licensing/licenses


Compilation
===========

Make sure you have ALGLIB installed. On Debian, you need the libalglib-dev
package.

To compile cmpsat, just type:

	$ bash make.sh


Usage
=====

To use cmpsat, type

	$ ./cmpsat data_file1 data_file2 num_used [bootstrapps]

num_used is the number of runtimes that will actually be used in the
comparison. It has to be less than the number of runtimes recorded for the
formula which can be found in the input file.

bootstrapps is the number of resamplings that will be used in bootstrap
estimate of the variance of r. If omitted or set to 0 jackknife estimate
will be used.

For sample data provided with cmpsat, one can run the comparison using 15
out of 50 available observations with jackknife estimate of the variance by
typing

	$ ./cmpsat examples/sample1 examples/sample2 15

Note: In this version the number of runtimes per formula should be the same
for both solvers. There is no theoretical reason for this. It is just the
current state of the program which is subject to change.


Input Format
============

One input file contains the data for one solver. It starts with the number of 
runtimes recorded for each formula. In each row of the input file, runtimes 
on one formula are recorded. Each runtime is followed by the indicator having 
value 1 if the runtime is exact, or 0 if it is censored. File containing 5 
observations for each of 2 formulae with used cutoff time of 1200 could look 
like this

	5
	533.23 1 1031.97 1 1200 0 1200 0 131.89 1
	981.37 1 1200 0 1200 0 1200 0 387.82 1


Output
======

cmpsat outputs values of several statistics:

 - n is the number of formulae that are not discarded in the comparison.
 - z is the difference between observed and the expected test statistic
   expressed in standard deviations.
 - r is the point biserial correlation estimate.
 - p is the p value for the test.
 - pi is the estimate of the probability that the first solver solves the
   formula in less time than the second.


Contact
=======

This version of cmpsat was modified by Vegard Nossum
<vegard.nossum@gmail.com>.

For all questions or suggestions concerning the original version of cmpsat
contact Mladen Nikolic <nikolic@matf.bg.ac.rs>.