For NP-hard problems such as SAT, even the best known algorithms have worst-case running times that increase exponentially as the problem size increases. In practice, however, many large instances of NP-hard problems still can be solved within a reasonable amount of time. In order to understand this phenomenon, much effort has been invested in understanding the "empirical hardness" of such problems.

 One recent approach uses linear basis function regression to obtain models of the time an algorithm will require to solve a given SAT instance. These empirical hardness models can be used to obtain insight into the factors responsible for an algorithm's performance, or to induce distributions of problem instances that are challenging for a given algorithm. They can also be leveraged to select among several different algorithms for
solving a given problem instance. Empirical hardness models have also proven very useful for combinatorial auctions, a prominent NP-hard optimization problem.  

  • First step of training a empirical hardness model is to collect  a SAT solver's runtime data for large set of instances.  Such solver can be a complete solver such as KCNFS, or SLS solver such as Nov+.
  • You also need compute some inexpensive features using as basis functions for linear regression. You can use our code to compute such features.
  • Just plug in linear regression. You can get a empirical hardness model.
  • For a new instances, you  do not have to solve it. Just compute the inexpensive features. Using your model, you can have pretty good idea how much time you will need to find out your instance is satisfiable or not.

Pretty cool, right?

For more information, visit our reading group at http://www.cs.ubc.ca/~hutter/EARG.shtml, or read some of our papers at http://www.cs.ubc.ca/~kevinlb/publications.html.

Getting started with empirical hardness models (we tested on Suse9, 10):

example.tar

There are lots of applications of using empirical hardness models. One example is satzilla:

satzilla

The new version of SATzilla --- SATzilla2007

For all insatnce

For random and handmade instance