Since 2014, several leading theoreticians and experimentalists conducting research on Boolean satisfiability (SAT) solving have been meeting annually to stimulate an increased exchange of ideas between these two communities. The hope has been for for a fruitful interplay between theoretical and experimental research in this area, with the belief that a more vigorous interaction between the two has potential for major long-term impact in computer science and mathematics, as well for applications in industry. in this fifth meeting of this group, it is appropriate to ask how successful has the interplay between theoretical and experimental research in SAT solving. In this brief talk, I will outline some areas of real progress. At the same, I will argue that progress has been rather mild relative to expectations, and suggest some concrete research directions that could be pursued to advance the theory and engineering of SAT solving.