Today, the design of electronic systems is largely automated. The practice of using software automation technologies for the design of electronic hardware is commonly referred to as Electronic Design Automation (EDA). EDA comprises a large set of tools, from languages that specify high-level hardware designs, to software that determines the layout of nanoscale devices on an integrated circuit. Within this collection, an important role is played by so-called logic synthesis algorithms. A substantial field of research onto itself, logic synthesis can be roughly thought of as the problem of finding good representations for Boolean functions. Such functions are the backbone of digital circuits, which can be thought of, to a first approximation, as devices that compute with Boolean values. In other words, circuits can be viewed simply as large Boolean functions. Logic synthesis, then, is assigned the important task of finding good structural representations for such circuits. Choosing the right logic synthesis algorithm can have a significant impact on the efficiency of an electronic design. In this thesis, we consider a special type of logic synthesis algorithm known as exact synthesis. Specifically, we analyze and develop multi-level exact synthesis algorithms based on a SAT formulation. Such algorithms attempt to solve a very difficult problem in which, given any Boolean function, they find the optimum (i.e. best possible) circuit that represents it. Our contributions can be roughly split into two parts: (i) core exact synthesis algorithms, and (ii) applications of exact synthesis. In the first part, we start by examining, in detail, different ways to encode the exact synthesis problem into CNF formulas. These formulas are given as input to SAT solvers, which solve them to find solutions. Finally, the solutions to these formulas can be decoded to obtain optimum Boolean circuits. We will compare and contrast the different encodings and show, quantitatively and experimentally, that a proper encoding can greatly influence the efficiency of exact synthesis algorithms. Next, we will show how such exact synthesis algorithms can be improved by adding domain-specific information. This information takes the form of families of DAG topologies which contain some additional structure to guide the SAT solver in its search. Furthermore, using these DAG topology families, we show how the exact synthesis problem can be transformed into an embarrassingly parallel one. This essentially means that, as long as we have processors available, we can throw more and more parallel computing power at the problem to solve it more quickly. After analyzing and improving the core exact synthesis algorithm, we arrive at the second part of the thesis. In this part, we show how exact synthesis can be applied to different problems that are of both theoretical and practical interest. On the theoretical side, we show how exact synthesis can be used to classify Boolean functions in terms of their intrinsic difficulty. On the practical side, we introduce a new data structure and logic representation called XOR-Majority Graphs (XMGs). We use XMGs, in concert with exact synthesis, to develop a novel logic rewriting methodology which achieves significant improvements over the state-of-the-art. We then generalize this methodology into one that can be used to restructure arbitrary Boolean networks, again enabling new improvements in logic synthesis.