Why do we use SAT solvers today? In 2001, they became fast enough that we can apply them to real-world problems.