Many applications of automated reasoning require decision procedures for the satisfiability of a formula in a theory given by the union of a few theories. Reasoning in a union of theories can be approached in more than one way. The equality-sharing method, also known as Nelson-Oppen scheme, combines decision procedures for the component theories. Superposition-based theorem-proving strategies unite the presentations of the theories to reason about their union. CDSAT, which stands for Conflict-Driven SATisfiability, assumes that each theory is equipped with an inference system, called theory module, and coordinates the theory modules to reason in a conflict-driven manner in the union of the theories. A theory module is an abstraction of a decision procedure, made of inference rules that may correspond to axioms of the theory. Conflict-driven means that the system maintains a representation of a candidate partial model of the formula, and performs nontrivial inferences only to explain conflicts between the candidate model and the formula, so that the conflict can be solved by updating the partial model. CDSAT provides a framework where the theory modules cooperate to build the candidate model and to explain the conflicts. This talk presents CDSAT placing it in the big picture of multi-theory reasoning and conflict-driven reasoning.