Isabelle solvers: "auto" or "fastforce"? (comparison of solver strength)

Question

In Isabelle, I often find that I can prove a goal successfully using different solvers.

Generally I would prefer to use the weakest solver that can just about prove the goal. Based on my experience with Isabelle so far, my current understanding is that in order of increasing strength and decreasing speed, the common logic solvers rank as follows (i.e. when rule and simp both work, rule should be used, etc.):

rule < simp < auto < fastforce < force

Is this correct? Where does blast fit in here?

I checked Programming and Proving in Isabelle/HOL (PDF) and Concrete Semantics with Isabelle/HOL but couldn't find the answer.

Answer 1

There generally is no linear ordering on the strength of proving methods and your word "weakest" assume there is one. We can nevertheless say that "auto" generally have at least the power of "simp" or "rule" but as it is more powerful it can also do some useless work that can make it fail. fastforce, bestsimp and slowsimp have the same power with different proof search strategies.

I can't really say more details on this, but maybe someone else could.