Most things I listed are pre-2007, minisat 2.2 had all but literal block distance. Which, I think, has proven itself since glucose replaced minisat in the hack thread.
You're probably right about the kitchen sink approach, however without it we probably wouldn't have MapleSat. MapleSat uses machine learning to replace the VSIDS heuristic. A bold move, but it has been replicated this year.
I checked (got curious about what ABC does): ABC uses minisat 2.2 as default and satoko (for 3 years) and glucose 3.0 (for 2 years) as options.
I don't know which configuration they used for the competitions. I think I saw "bmc -g" in some of the slides which would indicate glucose. However I also saw "abc super_solve" for which the name gives no information. (Maybe not the same years)
Indeed, smart applications of SAT solvers do more than raw performance.
Though, every little bit helps. Are you going to tell scientists what they should research? :)
You're probably right about the kitchen sink approach, however without it we probably wouldn't have MapleSat. MapleSat uses machine learning to replace the VSIDS heuristic. A bold move, but it has been replicated this year.
I checked (got curious about what ABC does): ABC uses minisat 2.2 as default and satoko (for 3 years) and glucose 3.0 (for 2 years) as options. I don't know which configuration they used for the competitions. I think I saw "bmc -g" in some of the slides which would indicate glucose. However I also saw "abc super_solve" for which the name gives no information. (Maybe not the same years)
Indeed, smart applications of SAT solvers do more than raw performance. Though, every little bit helps. Are you going to tell scientists what they should research? :)