  CNOT optimization plays a significant role in noise reduction for Quantum
Circuits. Several heuristic and exact approaches exist for CNOT optimization.
In this paper, we investigate more complicated variations of optimal synthesis
by allowing qubit permutations and handling layout restrictions. We encode such
problems into Planning, SAT, and QBF. We provide optimization for both CNOT
gate count and circuit depth. For experimental evaluation, we consider standard
T-gate optimized benchmarks and optimize CNOT sub-circuits. We show that
allowing qubit permutations can further reduce up to 56% in CNOT count and 46%
in circuit depth. In the case of optimally mapped circuits under layout
restrictions, we observe a reduction up to 17% CNOT count and 19% CNOT depth.
