Recent studies show that majority-based logic synthesis is beneficial for both traditional and nanotechnology digital designs. However, most of the existing synthesis algorithms for majority logic generate majority-of-three (M-3) networks. The optimization opportunity for majority logic by using an arbitrary number of odd inputs still requires a large research effort. In this paper, we present an exact synthesis approach for computing Boolean functions in majority-of-five (M-5) forms with a minimum number of operations using Boolean satisfiability. By exploiting the symmetry properties of majority operators, we make use of symbolic encoding method to represent the node functionality and to reduce the number of variables. Moreover, we represent the M-5 forms by M-5-inverter graphs (M(5)IGs) for manipulation, which is an extension of majority-inverter graphs (MIGs). The experimental results on EPFL benchmark suites indicate the proposed method achieves 10.4 % improvement on size and 11.4 % on depth compared to the state-of-the-art exact synthesis method.