{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T00:43:20Z","timestamp":1778028200454,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,1,16]],"date-time":"2023-01-16T00:00:00Z","timestamp":1673827200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101001318"],"award-info":[{"award-number":["101001318"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,1,16]]},"DOI":"10.1145\/3566097.3567929","type":"proceedings-article","created":{"date-parts":[[2023,1,31]],"date-time":"2023-01-31T18:40:49Z","timestamp":1675190449000},"page":"190-195","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["A SAT Encoding for Optimal Clifford Circuit Synthesis"],"prefix":"10.1145","author":[{"given":"Sarah","family":"Schneider","sequence":"first","affiliation":[{"name":"Johannes Kepler University Linz, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lukas","family":"Burgholzer","sequence":"additional","affiliation":[{"name":"Johannes Kepler University Linz, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Wille","sequence":"additional","affiliation":[{"name":"Technical University of Munich, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,1,31]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/1972505"},{"key":"e_1_3_2_2_2_1","volume-title":"of the ACM","author":"Grover L. K.","year":"1996","unstructured":"L. K. Grover, \"A fast quantum mechanical algorithm for database search,\" Proc. of the ACM, 1996."},{"key":"e_1_3_2_2_3_1","volume-title":"The basis of design tools for quantum computing,\" in Design Automation Conf","author":"Wille R.","year":"2022","unstructured":"R. Wille et al., \"The basis of design tools for quantum computing,\" in Design Automation Conf., 2022."},{"key":"e_1_3_2_2_4_1","author":"Barenco A.","year":"1995","unstructured":"A. Barenco et al., \"Elementary gates for quantum computation,\" Phys. Rev. A, 1995.","journal-title":"Phys. Rev. A"},{"key":"e_1_3_2_2_5_1","author":"Maslov D.","year":"2016","unstructured":"D. Maslov, \"On the advantages of using relative phase Toffolis with an application to multiple control Toffoli optimization,\" Phys. Rev. A, 2016.","journal-title":"Phys. Rev. A"},{"key":"e_1_3_2_2_6_1","volume-title":"Improving the mapping of reversible circuits to quantum circuits using multiple target lines,\" in Asia and South Pacific Design Automation Conf","author":"Wille R.","year":"2013","unstructured":"R. Wille, M. Soeken, C. Otterstedt, and R. Drechsler, \"Improving the mapping of reversible circuits to quantum circuits using multiple target lines,\" in Asia and South Pacific Design Automation Conf., 2013."},{"key":"e_1_3_2_2_7_1","volume-title":"Architecture-aware synthesis of phase polynomials for NISQ devices","author":"de Griend A.","year":"2020","unstructured":"A. M.-v. de Griend and R. Duncan, Architecture-aware synthesis of phase polynomials for NISQ devices, 2020. arXiv: 2004.06052."},{"key":"e_1_3_2_2_8_1","unstructured":"D. Gottesman \"Stabilizer codes and quantum error correction. \" Caltech 1997."},{"key":"e_1_3_2_2_9_1","volume-title":"Prog. Phys.","author":"Devitt S. J.","year":"2013","unstructured":"S. J. Devitt, K. Nemoto, and W. J. Munro, \"Quantum error correction for beginners,\" Rep. Prog. Phys., 2013."},{"key":"e_1_3_2_2_10_1","volume-title":"6-qubit optimal Clifford circuits","author":"Bravyi S.","year":"2020","unstructured":"S. Bravyi, J. A. Latone, and D. Maslov, 6-qubit optimal Clifford circuits, 2020. arXiv: 2012.06074."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1550723"},{"key":"e_1_3_2_2_12_1","volume-title":"Mapping quantum circuits to IBM QX architectures using the minimal number of SWAP and H operations,\" in Design Automation Conf","author":"Wille R.","year":"2019","unstructured":"R. Wille, L. Burgholzer, and A. Zulehner, \"Mapping quantum circuits to IBM QX architectures using the minimal number of SWAP and H operations,\" in Design Automation Conf., 2019."},{"key":"e_1_3_2_2_13_1","volume-title":"Optimal layout synthesis for quantum computing,\" in Int'l Conf. on CAD","author":"Tan B.","year":"2020","unstructured":"B. Tan and J. Cong, \"Optimal layout synthesis for quantum computing,\" in Int'l Conf. on CAD, 2020."},{"key":"e_1_3_2_2_14_1","volume-title":"Conf. Theory Appl. Satisf. Test.","author":"Berent L.","year":"2022","unstructured":"L. Berent, L. Burgholzer, and R. Wille, \"Towards a SAT encoding for quantum circuits: A journey from classical circuits to Clifford circuits and beyond,\" in Int. Conf. Theory Appl. Satisf. Test., 2022. arXiv: 2203.00698."},{"key":"e_1_3_2_2_15_1","volume-title":"Fast equivalence-checking for quantum circuits,\" in Intl Symp Nanoscale Archit","author":"Yamashita S.","year":"2010","unstructured":"S. Yamashita and I. L. Markov, \"Fast equivalence-checking for quantum circuits,\" in Intl Symp Nanoscale Archit., 2010."},{"key":"e_1_3_2_2_16_1","volume-title":"Reducing the overhead of mapping quantum circuits to IBM Q system,\" in IEEE International Symposium on Circuits and Systems","author":"Matsuo A.","year":"2019","unstructured":"A. Matsuo, W. Hattori, and S. Yamashita, \"Reducing the overhead of mapping quantum circuits to IBM Q system,\" in IEEE International Symposium on Circuits and Systems, 2019."},{"key":"e_1_3_2_2_17_1","volume-title":"T} quantum circuit synthesis,\" in Int'l Conf. of Reversible Computation","author":"Meuli G.","year":"2018","unstructured":"G. Meuli, M. Soeken, and G. Micheli, \"SAT-based {CNOT, T} quantum circuit synthesis,\" in Int'l Conf. of Reversible Computation, 2018."},{"key":"e_1_3_2_2_18_1","volume-title":"Limiting the search space in optimal quantum circuit mapping,\" in Asia and South Pacific Design Automation Conf","author":"Burgholzer L.","year":"2022","unstructured":"L. Burgholzer, S. Schneider, and R. Wille, \"Limiting the search space in optimal quantum circuit mapping,\" in Asia and South Pacific Design Automation Conf., 2022."},{"key":"e_1_3_2_2_19_1","volume-title":"ATPG for reversible circuits using simulation, boolean satisfiability, and pseudo boolean optimization,\" in IEEE Annual Symp. on VLSI","author":"Wille R.","year":"2011","unstructured":"R. Wille, H. Zhang, and R. Drechsler, \"ATPG for reversible circuits using simulation, boolean satisfiability, and pseudo boolean optimization,\" in IEEE Annual Symp. on VLSI, 2011."},{"key":"e_1_3_2_2_20_1","volume-title":"Clifford circuit optimization with templates and symbolic Pauli gates,\" Quantum","author":"Bravyi S.","year":"2021","unstructured":"S. Bravyi, R. Shaydulin, S. Hu, and D. Maslov, \"Clifford circuit optimization with templates and symbolic Pauli gates,\" Quantum, 2021. arXiv: 2105.02291."},{"key":"e_1_3_2_2_21_1","volume-title":"Qiskit: An open-source framework for quantum computing,\" Zenodo","author":"Aleksandrowicz G.","year":"2019","unstructured":"G. Aleksandrowicz et al., \"Qiskit: An open-source framework for quantum computing,\" Zenodo, 2019."},{"key":"e_1_3_2_2_22_1","author":"Aaronson S.","year":"2004","unstructured":"S. Aaronson and D. Gottesman, \"Improved simulation of stabilizer circuits,\" Phys. Rev. A, 2004.","journal-title":"\"Improved simulation of stabilizer circuits,\" Phys. Rev. A"},{"key":"e_1_3_2_2_23_1","volume-title":"The Heisenberg representation of quantum computers","author":"Gottesman D.","year":"1998","unstructured":"D. Gottesman, The Heisenberg representation of quantum computers, 1998. arXiv: quantph\/9807006."},{"key":"e_1_3_2_2_24_1","volume-title":"Efficient synthesis of quantum circuits implementing Clifford group operations,\" in Asia and South Pacific Design Automation Conf","author":"Niemann P.","year":"2014","unstructured":"P. Niemann, R. Wille, and R. Drechsler, \"Efficient synthesis of quantum circuits implementing Clifford group operations,\" in Asia and South Pacific Design Automation Conf., 2014."},{"key":"e_1_3_2_2_25_1","first-page":"1305","author":"Kliuchnikov V.","year":"2013","unstructured":"V. Kliuchnikov and D. Maslov, \"Optimization of Clifford circuits,\" Phys. Rev. A, 2013. arXiv: 1305.0810.","journal-title":"\"Optimization of Clifford circuits,\" Phys. Rev. A"},{"key":"e_1_3_2_2_26_1","volume-title":"Z3: An efficient SMT solver,\" in Tools Algorithms Constr. Anal. Syst","author":"de Moura L.","year":"2008","unstructured":"L. de Moura and N. Bj\u00f8rner, \"Z3: An efficient SMT solver,\" in Tools Algorithms Constr. Anal. Syst., Springer, 2008."},{"key":"e_1_3_2_2_27_1","volume-title":"OptiMathSAT: A tool for optimization modulo theories,\" J Autom Reasoning","author":"Sebastiani R.","year":"2020","unstructured":"R. Sebastiani and P. Trentin, \"OptiMathSAT: A tool for optimization modulo theories,\" J Autom Reasoning, 2020."}],"event":{"name":"ASPDAC '23: 28th Asia and South Pacific Design Automation Conference","location":"Tokyo Japan","acronym":"ASPDAC '23","sponsor":["SIGDA ACM Special Interest Group on Design Automation","IEEE CEDA","IEICE","IEEE CAS","IPSJ"]},"container-title":["Proceedings of the 28th Asia and South Pacific Design Automation Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3566097.3567929","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3566097.3567929","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T17:33:56Z","timestamp":1767807236000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3566097.3567929"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,16]]},"references-count":27,"alternative-id":["10.1145\/3566097.3567929","10.1145\/3566097"],"URL":"https:\/\/doi.org\/10.1145\/3566097.3567929","relation":{},"subject":[],"published":{"date-parts":[[2023,1,16]]},"assertion":[{"value":"2023-01-31","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}