Read Me

AvatarSAT
=========

AvatarSAT is a SAT solver that uses machine-learning classifiers to
automatically tune the heuristics of an off-the-shelf SAT solver on a
per-instance basis. The classifiers use features of both the input and
conflict clauses to select parameter settings for the solver's tunable
heuristics.

On a randomly selected set of SAT problems chosen from the 2007 and
2008 SAT competitions, AvatarSAT is, on the average, three times
faster per problem than MiniSAT based on the geometric mean speedup
measure and two times faster per problem based on the arithmetic mean
speedup measure. Moreover, AvatarSAT is hundreds to thousands of times
faster than MiniSAT on many hard SAT instances and is never more than
twenty times slower than MiniSAT on any SAT instance.

AvatarSAT is distributed under the MIT license.


Usage
======

AvatarSAT can be built and then invoked on a cnf file as follows:

$ make
$ ./bin/avatarsat <cnf filename>

Model files are required for AvatarSAT to run. By default, AvatarSAT
looks for these files in /usr/local/share/avatarsat and in the models
directory in the location where you extracted the AvatarSAT
archive. If you do not move this directory, AvatarSAT should have no
trouble finding these files. You can specify alternative model files
using the following command-line options:

  -correction-model-file=        specify model for course correction
  -preprocessor-model-file=      specify model for preprocessor
  -correction-range-file=        specify range for course correction
  -preprocessor-range-file=      specify range for preprocessor