Bridging Two Communities to Solve Real Problems

This paper is an extended abstract of an invited talk of the samename, given at SYNASC 2016. It describes a sort of case study of howideas from computational logic (specifically Satisfiability ModuloTheory solving) provide new algorithms in symbolic computing. Inparticular, it describes how ideas from the NLSAT solver led to a newkind of Cylindrical Algebraic Decomposition.