For the past 40 years computer scientists generally believed thatNP-complete problems are intractable. In particular, Booleansatisfiability (SAT), as a paradigmatic automated-reasoning problem, hasbeen considered to be intractable. Over the past 20 years, however, therehas been a quiet, but dramatic, revolution, and very large SAT instancesare now being solved routinely as part of software and hardware design.In this talk I will review this amazing development and show how automatedreasoning is now an industrial reality.I will then describe how we can leverage SAT solving to accomplishother automated-reasoning tasks. Counting the the number of satisfyingtruth assignments of a given Boolean formula or sampling such assignmentsuniformly at random are fundamental computational problems in computerscience with applications in software testing, software synthesis, machinelearning, personalized learning, and more. While the theory of theseproblems has been thoroughly investigated since the 1980s, approximationalgorithms developed by theoreticians do not scale up to industrial-sizedinstances. Algorithms used by the industry offer better scalability,but give up certain correctness guarantees to achieve scalability. Wedescribe a novel approach, based on universal hashing and SatisfiabilityModulo Theory, that scales to formulas with hundreds of thousands ofvariables without giving up correctness guarantees.