Paper on SMT encodings for quantum circuit optimization, with exact-G and null-gate variants that synthesize S-box circuits faster than e...