Abstract
Despite well-meaning diligent efforts to foster collaboration between SAT theoreticians and SAT practitioners over the last two decades, these two communities have mostly remained securely in their own echo chambers. In this talk I hope to start a conversation about ways to remedy this situation by encouraging a prgamatic problem-solving approach for conducting SAT research. Recognizing that SAT instances encoding human-created artifacts are not random suggests the possibility of adapting SAT solving strategies to the structural properties of these artifacts. This will yield algorithmic solver innovations supported by practical theoretical analysis of different classes of SAT formulas.