We propose effective algorithms for exact synthesis of Boolean logic networks using satisfiability modulo theories (SMT) solvers. Since exact synthesis is a difficult problem, it can only be applied efficiently to very small functions, having up to 6 variables. Key in our approach is to use majority-inverter graphs as underlying logic representation as they are simple (homogeneous logic representation) and expressive (contain And/Or-inverter graphs) at the same time. This has a positive impact on the problem formulation: it simplifies the encoding as SMT constraints and also allows for various techniques to break symmetries in the search space due to the regular data structure. Our algorithm optimizes with respect to the MIG’s size or depth and uses different ways to encode the problem and several methods to improve solving time, with symmetry breaking techniques being the most effective ones. We discuss several applications of exact synthesis and motivate them by experiments on a set of large arithmetic benchmarks. Using the proposed techniques, we are able to improve both area and delay after LUT-based technology mapping beyond the current results achieved by state-of-the-art logic synthesis algorithms.