About 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.

Downloads

• AvatarSAT source
• Some example CNF files used in testing
• The LibSVM models used in testing
• The output of AvatarSAT and MiniSAT 2.0 on our test cases