This example plot compares VARSAT and default MiniSat on hard random problems of increasing size. VARSAT is built within MiniSat but during execution it continually calculates statistical information for use in variable- and value-ordering heuristics. Here VARSAT is represented by "EMSP-G," the overall most effective of these heuristics to be developed so far.

For each problem size marked in the graph, the two solvers were run on 1000 satisfiable instances that were randomly generated with a clause-to-variable ratio of 4.11--such problems represent the hard region of the satisfiability phase transition. The average runtime on such problems is plotted in log-scale. The last two data points for default MiniSat represent lower bounds; on a percentage of the runs MiniSat timed out by failing to solve an instance within 10,800 seconds (three hours.)

A variety of experiments, measuring different characteristics of multiple techniques on assorted problem types, can be found here.