The SAT (Boolean Satisfiability) problem asks whether a given logical formula on n Boolean variables has an assignment of true/false values to its variables that makes the formula true.  The P vs NP question is equivalent to asking whether SAT has a "fast" algorithm, running in polynomial time in n. In spite of the revolution in practical SAT solving that has occurred over the last two decades, it remains a major open problem in computer science (and mathematics) to find an algorithm for SAT that provably beats (even slightly) exhaustive search over all 2n possibilities. In this talk, I will describe my dogged pursuit of such an algorithm and my various failures to find one, which led to new connections, research areas, and strange intellectual surprises. In one direction, we found that computational hardness results can be derived from SAT algorithms which beat exhaustive search. This is the core idea in the "algorithmic method", an approach which has produced long-sought hardness results for certain types of algorithms, through faster than brute-force algorithms for related classes of formulas. In another direction, we found that improving upon the best known efficient (in P) algorithms for some "easy" problems (e.g., computing shortest paths in simple graphs) would yield better than brute-force SAT algorithms. Such results are a part of a growing area called "fine-grained complexity" which tries to understand which textbook algorithms are optimal, and what would be the consequences for improving them. No special background knowledge will be assumed.