What's the problem this feature will solve?

Pauli gates can always be pushed to the end of the circuit when synthesizing Clifford circuits. At the moment Pauli gates are explicitely considered at every depth in the encoding which unnecessarily increases the size of the formulation and the search space.

Describe the solution you'd like

Since the Pauli gates only ever change the Phase of the stabilizer tableau, all constraints on the phase and the phase variables themselves can be dropped in the encoding. After circuit synthesis, the phases can be corrected by simulating the circuit and flipping phases with the appropriate Pauli gate.