An Auto-tuning SAT Solver

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.


Rishabh Singh (PhD Student at MIT, Cambridge, MA, USA)
Joseph P. Near (PhD Student at MIT, Cambridge, MA, USA)
Dr. Vijay Ganesh (Research Scientist at MIT, Cambridge, MA, USA)


  • AvatarSAT is based on MiniSAT
  • AvatarSAT uses LibSVM for machine learning