One interesting thing about advances in SAT solvers is that they often translate into advances in other areas. There was this one period in AI planning when people got an order of magnitude speedups by translating planning problems into SAT and running them on SAT solvers (this was embarrassing, so advances in pure planners followed within a year).
Now people are converting graphical model structure learning problems into SAT (there was a talk about this at UAI this year).
“Can a SAT solver do it faster than your entire area?” is a good sanity check.
Minor note: while this is true for many areas, some areas like physics simulations don’t have this sort of sanity check because there are no known witnesses to a correct calculation.
One interesting thing about advances in SAT solvers is that they often translate into advances in other areas. There was this one period in AI planning when people got an order of magnitude speedups by translating planning problems into SAT and running them on SAT solvers (this was embarrassing, so advances in pure planners followed within a year).
Now people are converting graphical model structure learning problems into SAT (there was a talk about this at UAI this year).
“Can a SAT solver do it faster than your entire area?” is a good sanity check.
Minor note: while this is true for many areas, some areas like physics simulations don’t have this sort of sanity check because there are no known witnesses to a correct calculation.