5
$\begingroup$

CASC is the premier Automated Theorem Prover competition performed annually at the Conference on Automated Deduction (CADE). The 2017 event has finished on the 9th of August this year.

During this conference provers are faced with a set of problems and a time limit of 5 minutes (300 seconds) per problem. When the competition is over, the timings for each problem are taken to produce performance plots. enter image description here

Here we see the results from the general first order formulas (FOF) division. 11 ATP systems participated, Vampire 4.2 was the winner in this division having solved over 450 problems from the set.

It is clear from this plot that the timings for each prover were independently sorted in increasing order and plotted over the same axes.

What is puzzling is the shape of the graph: for most provers most of the problems were really easy (solved within 50 seconds) and only a small proportion of problems were difficult yet solvable within the time limit (i.e. about 5% for Vampire 4.2 and less than 10% for Vampire 4.0, the 2016 winner). On the remaining problems (there were 500 problems altogether) the prover failed. Is there an intuitively simple explanation of why the difficulty distribution is so skewed towards "easy" problems not for one but for all provers?

$\endgroup$
3
$\begingroup$

I can speculate/hypothesize. Each solver has many heuristics and proof tactics. Imagine that corresponding to each heuristic is a class of instances that are easy to solve if you use that heuristic, but hard if you don't (e.g., if you don't have a heuristic for it and you fall back to the generic methods, maybe you're effectively exploring the entire exponentially large space of possible solutions to try to find one that works). An example would be 2SAT; if you use the right algorithm, it can be solved in linear time, but if you blindly search, that will take exponential time.

So, in this model, if an instance is handled by one of the prover's heuristics, it is solved very rapidly; otherwise you fall back to some generic method that may take exponential time. This would lead to a kind of "very fast or very slow" dichotomy. And the set of instances that a prover is fast on may be different for each prover, because prover uses a different set of heuristics. In other words, this hypothesis would explain the observed behavior.

I have no data and no hard evidence, so this is merely speculation. It could be entirely wrong.

$\endgroup$
  • 1
    $\begingroup$ There's likely a power law distribution in the "difficulty" in some suitable sense of the test problems. $\endgroup$ – Derek Elkins Aug 11 '17 at 1:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.