The prospective of practical quantum computers has lead researchers to investigate automatic tools to program them. A quantum program is modeled as a Clifford+T quantum circuit that needs to be optimized in order to comply with quantum technology constraints. Most of the optimization algorithms aim at reducing the number of T gates. Nevertheless, a secondary optimization objective should be to minimize the number of two-qubit operations (the CNOT gates) as they show lower fidelity and higher error rate when compared to single-qubit operations. We have developed an exact SAT-based algorithm for quantum circuit rewriting that aims at reducing CNOT gates without increasing the number of T gates. Our algorithm finds the minimum {CNOT, T} circuit for a given phase polynomial description of a unitary transformation. Experiments confirm a reduction of CNOT in T-optimized quantum circuits. We synthesize quantum circuits for all single-target gates whose control functions are one of the representatives of the 48 spectral equivalence classes of all 5-input Boolean functions. Our experiments show an average CNOT reduction of 26.84%.