{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:13:16Z","timestamp":1775790796727,"version":"3.50.1"},"publisher-location":"Cham","reference-count":77,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656323","type":"print"},{"value":"9783031656330","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Quantum circuit compilation comprises many computationally hard reasoning tasks that lie inside #<jats:inline-formula><jats:alternatives><jats:tex-math>$${\\textsf{P}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>P<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>and its decision counterpart in\u00a0<jats:inline-formula><jats:alternatives><jats:tex-math>$${\\textsf{PP}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>PP<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>. The classical simulation of universal quantum circuits is a core example. We show for the first time that a strong simulation of universal quantum circuits can be efficiently tackled through weighted model counting by providing a linear-length encoding of Clifford+<jats:italic>T<\/jats:italic>circuits. To achieve this, we exploit the stabilizer formalism by Knill, Gottesmann, and Aaronson by reinterpreting quantum states as a linear combination of stabilizer states. With an open-source simulator implementation, we demonstrate empirically that model counting often outperforms state-of-the-art simulation techniques based on the ZX calculus and decision diagrams. Our work paves the way to apply the existing array of powerful classical reasoning tools to realize efficient quantum circuit compilation; one of the obstacles on the road towards quantum supremacy.<\/jats:p>","DOI":"10.1007\/978-3-031-65633-0_25","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:08Z","timestamp":1721890988000},"page":"555-578","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Simulating Quantum Circuits by\u00a0Model Counting"],"prefix":"10.1007","author":[{"given":"Jingyi","family":"Mei","sequence":"first","affiliation":[]},{"given":"Marcello","family":"Bonsangue","sequence":"additional","affiliation":[]},{"given":"Alfons","family":"Laarman","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"Akers. Binary decision diagrams. IEEE Trans. Comput. C-27(6), 509\u2013516 (1978)","DOI":"10.1109\/TC.1978.1675141"},{"key":"25_CR2","doi-asserted-by":"publisher","first-page":"343","DOI":"10.4204\/EPTCS.394.17","volume":"394","author":"M Amy","year":"2023","unstructured":"Amy, M., Bennett-Gibbs, O., Ross, N.J.: Symbolic synthesis of Clifford circuits and beyond. Electron. Proc. Theor. Comput. Sci. 394, 343\u2013362 (2023)","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Anders, S., Briegel, H.J.: Fast simulation of stabilizer circuits using a graph-state representation. Phys. Rev. A 73(2) (2006)","DOI":"10.1103\/PhysRevA.73.022334"},{"key":"25_CR4","unstructured":"Hecher, M., Fichte, J.: Model counting competition (2023). https:\/\/mccompetition.org\/. Accessed 01 Jul 2024"},{"key":"25_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-642-36742-7_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Ardeshir-Larijani","year":"2013","unstructured":"Ardeshir-Larijani, E., Gay, S.J., Nagarajan, R.: Equivalence checking of quantum protocols. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 478\u2013492. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_33"},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/978-3-642-54862-8_42","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Ardeshir-Larijani","year":"2014","unstructured":"Ardeshir-Larijani, E., Gay, S.J., Nagarajan, R.: Verification of concurrent quantum protocols by equivalence checking. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 500\u2013514. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_42"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/978-3-642-54862-8_42","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Ardeshir-Larijani","year":"2014","unstructured":"Ardeshir-Larijani, E., Gay, S.J., Nagarajan, R.: Verification of concurrent quantum protocols by equivalence checking. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 500\u2013514. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_42"},{"key":"25_CR8","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1038\/s41586-019-1666-5","volume":"574","author":"F Arute","year":"2019","unstructured":"Arute, F., et al.: Quantum supremacy using a programmable superconducting processor. Nature 574, 505\u2013510 (2019)","journal-title":"Nature"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"Iris Bahar, R., et al.: Algebraic decision diagrams and their applications. In: Proceedings of 1993 International Conference on Computer Aided Design (ICCAD), pp. 188\u2013191 (1993)","DOI":"10.1109\/ICCAD.1993.580054"},{"key":"25_CR10","doi-asserted-by":"publisher","unstructured":"Bauer-Marquart, F., Leue, S., Schilling, C.: symQV: automated symbolic verification of quantum programs. In: Chechik, M., Katoen, J.-P., Leucker, M., ed, Formal Methods, pp. 181\u2013198. Springer International Publishing, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_12","DOI":"10.1007\/978-3-031-27481-7_12"},{"key":"25_CR11","unstructured":"Berent, L., Burgholzer, L., Wille, R.: Towards a SAT encoding for quantum circuits: a journey from classical circuits to clifford circuits and beyond. In: Meel, K.S., Strichman, O., ed., 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022), volume 236 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 18:1\u201318:17, Dagstuhl, Germany (2022). Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik"},{"key":"25_CR12","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T., ed. Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press (2009)"},{"key":"25_CR13","unstructured":"Brand, S., Coopmans, T., Laarman, A.: Quantum graph-state synthesis with SAT. In: Proceedings of the 14th International Workshop on Pragmatics of SAT co-located with the 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023), Alghero, Italy, July 4, 2023, volume 3545 of CEUR Workshop Proceedings, pp. 1\u201313. CEUR-WS.org (2023)"},{"key":"25_CR14","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.116.250501","volume":"116","author":"S Bravyi","year":"2016","unstructured":"Bravyi, S., Gosset, D.: Improved classical simulation of quantum circuits dominated by Clifford gates. Phys. Rev. Lett. 116, 250501 (2016)","journal-title":"Phys. Rev. Lett."},{"key":"25_CR15","doi-asserted-by":"publisher","first-page":"580","DOI":"10.22331\/q-2021-11-16-580","volume":"5","author":"S Bravyi","year":"2021","unstructured":"Bravyi, S., Shaydulin, R., Shaohan, H., Maslov, D.: Clifford circuit optimization with templates and symbolic Pauli gates. Quantum 5, 580 (2021)","journal-title":"Quantum"},{"issue":"8","key":"25_CR16","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"Burgholzer, L., Wille, R.: Improved DD-based equivalence checking of quantum circuits. In: 2020 25th Asia and South Pacific Design Automation Conference (ASP-DAC), pp. 127\u2013132. IEEE (2020)","DOI":"10.1109\/ASP-DAC47756.2020.9045153"},{"key":"25_CR18","doi-asserted-by":"publisher","first-page":"1098","DOI":"10.1103\/PhysRevA.54.1098","volume":"54","author":"AR Calderbank","year":"1996","unstructured":"Calderbank, A.R., Shor, P.W.: Good quantum error-correcting codes exist. Phys. Rev. A 54, 1098\u20131105 (1996)","journal-title":"Phys. Rev. A"},{"key":"25_CR19","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Fremont, D., Meel, K., Seshia, S., Vardi, M.: Distribution-aware sampling and weighted model counting for sat. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a028 (2014)","DOI":"10.1609\/aaai.v28i1.8990"},{"issue":"6","key":"25_CR20","doi-asserted-by":"publisher","first-page":"772","DOI":"10.1016\/j.artint.2007.11.002","volume":"172","author":"M Chavira","year":"2008","unstructured":"Chavira, M., Darwiche, A.: On probabilistic inference by weighted model counting. Artif. Intell. 172(6), 772\u2013799 (2008)","journal-title":"Artif. Intell."},{"key":"25_CR21","unstructured":"Chen, Y., Chen, Y., Kumar, R., Patro, S., Speelman, F.: QSETH strikes again: finer quantum lower bounds for lattice problem, strong simulation, hitting set problem, and more. arXiv preprint arXiv:2309.16431 (2023)"},{"key":"25_CR22","doi-asserted-by":"crossref","unstructured":"Chen, Y.-F., Chung, K.-M., Leng\u00e1l, O., Lin, J.-A., Tsai, W.-L., Yen, D.-D.: An automata-based framework for verification and bug hunting in quantum circuits. Proc. ACM Program. Lang., 7(PLDI) (2023)","DOI":"10.1145\/3591270"},{"key":"25_CR23","doi-asserted-by":"publisher","unstructured":"Chen, Y.-F., R\u00fcmmer, P., Tsai, W.-L.: A theory of cartesian arrays (with applications in quantum circuit verification). In: International Conference on Automated Deduction, pp. 170\u2013189. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_10","DOI":"10.1007\/978-3-031-38499-8_10"},{"key":"25_CR24","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., McMillan, K.L., Zhao, X., Fujita, M., Yang, J.: Spectral transforms for large Boolean functions with applications to technology mapping. In: Proceedings of the 30th international Design Automation Conference, pp. 54\u201360 (1993)","DOI":"10.1145\/157485.164569"},{"issue":"4","key":"25_CR25","doi-asserted-by":"publisher","DOI":"10.1088\/1367-2630\/13\/4\/043016","volume":"13","author":"B Coecke","year":"2011","unstructured":"Coecke, B., Duncan, R.: Interacting quantum observables: categorical algebra and diagrammatics. New J. Phys. 13(4), 043016 (2011)","journal-title":"New J. Phys."},{"issue":"3","key":"25_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3505636","volume":"3","author":"A Cross","year":"2022","unstructured":"Cross, A., et al.: OpenQASM3: a broader and deeper quantum assembly language. ACM Trans. Quantum Comput. 3(3), 1\u201350 (2022)","journal-title":"ACM Trans. Quantum Comput."},{"issue":"1","key":"25_CR27","first-page":"81","volume":"6","author":"CM Dawson","year":"2006","unstructured":"Dawson, C.M., Nielsen, M.A.: The Solovay-Kitaev algorithm. Quantum Inf. Comput. 6(1), 81\u201395 (2006)","journal-title":"Quantum Inf. Comput."},{"issue":"3","key":"25_CR28","first-page":"258","volume":"10","author":"M Van den Nest","year":"2010","unstructured":"Van den Nest, M.: Classical simulation of quantum computation, the gottesman-knill theorem, and slightly beyond. Quantum Inf. Comput. 10(3), 258\u2013271 (2010)","journal-title":"Quantum Inf. Comput."},{"key":"25_CR29","unstructured":"Ermon, S., Gomes, C.P., Sabharwal, A., Selman, B.: Embed and project: discrete sampling with universal hashing. In: Advances in Neural Information Processing Systems, vol. 26 (2013)"},{"key":"25_CR30","doi-asserted-by":"publisher","unstructured":"Feng, N., Marsso, L., Sabetzadeh, M., Chechik, M.: Early verification of legal compliance via bounded satisfiability checking. In: Enea, C., Lal, A., ed., Computer Aided Verification, pp. 374\u2013396. Springer Nature Switzerland, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_18","DOI":"10.1007\/978-3-031-37709-9_18"},{"key":"25_CR31","doi-asserted-by":"crossref","unstructured":"Fisher, M.P.A., Khemani, V., Nahum, A., Vijay, S.: Random quantum circuits. Ann. Rev. Condensed Matter Phys. 14(1), 335\u2013379 (2023)","DOI":"10.1146\/annurev-conmatphys-031720-030658"},{"key":"25_CR32","doi-asserted-by":"crossref","unstructured":"Garc\u00eda, H.J., Markov, I.L., Cross, A.W.: On the geometry of stabilizer states. Quantum Inf. Comput. 14(7 &8), 683\u2013720 (2014)","DOI":"10.26421\/QIC14.7-8-9"},{"key":"25_CR33","unstructured":"Gay, S.J.: Stabilizer states as a basis for density matrices. CoRR, abs\/1112.2156 (2011)"},{"key":"25_CR34","unstructured":"Golia, P., Soos, M., Chakraborty, S., Meel, K.S.: Designing samplers is easy: The boon of testers. In: 2021 Formal Methods in Computer Aided Design (FMCAD), pp. 222\u2013230. IEEE (2021)"},{"key":"25_CR35","unstructured":"Gottesman, D.: Stabilizer codes and quantum error correction. PhD thesis, California Institute of Technology (1997)"},{"key":"25_CR36","unstructured":"Hashimoto, K.: GPMC (2020). https:\/\/git.trs.css.i.nagoya-u.ac.jp\/k-hasimt\/GPMC"},{"key":"25_CR37","doi-asserted-by":"crossref","unstructured":"Hong, X., Feng, Y., Li, S., Ying, M.: Equivalence checking of dynamic quantum circuits. In: Proceedings of the 41st IEEE\/ACM International Conference on Computer-Aided Design, ICCAD \u201922, New York, NY, USA (2022). Association for Computing Machinery","DOI":"10.1145\/3508352.3549479"},{"key":"25_CR38","doi-asserted-by":"crossref","unstructured":"Hong, X., Zhou, X., Li, S., Feng, Y., Ying, M.: A tensor network based decision diagram for representation of quantum circuits. ACM Trans. Design Autom. Electr. Syst. 27(6), 60:1\u201360:30 (2022)","DOI":"10.1145\/3514355"},{"key":"25_CR39","unstructured":"Huang, C., et al.: Classical simulation of quantum supremacy circuits, Mario Szegedy (2020)"},{"issue":"7\u20138","key":"25_CR40","first-page":"633","volume":"14","author":"R Jozsa","year":"2014","unstructured":"Jozsa, R., Van den Nest, M.: Classical simulation complexity of extended Clifford circuits. Quantum Inf. Comput. 14(7\u20138), 633\u2013648 (2014)","journal-title":"Quantum Inf. Comput."},{"issue":"4","key":"25_CR41","doi-asserted-by":"publisher","DOI":"10.1088\/2058-9565\/ac5d20","volume":"7","author":"A Kissinger","year":"2022","unstructured":"Kissinger, A., van de Wetering, J.: Simulating quantum circuits with ZX-calculus reduced stabiliser decompositions. Quantum Sci. Technol. 7(4), 044001 (2022)","journal-title":"Quantum Sci. Technol."},{"key":"25_CR42","unstructured":"Kliuchnikov, V.: Synthesis of unitaries with Clifford+T circuits. arXiv e-prints arXiv:1306.3200 (2013)"},{"key":"25_CR43","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.103.022603","volume":"103","author":"L Kocia","year":"2021","unstructured":"Kocia, L., Sarovar, M.: Classical simulation of quantum circuits using fewer gaussian eliminations. Phys. Rev. A 103, 022603 (2021)","journal-title":"Phys. Rev. A"},{"key":"25_CR44","doi-asserted-by":"crossref","unstructured":"Lai, Y.-T., Pedram, M., Vrudhula, S.B.K.: EVBDD-based algorithms for integer linear programming, spectral transformation, and function decomposition. IEEE Trans. Comput.-Aid. Design Integr. Circ. Syst. 13(8), 959\u2013975 (1994)","DOI":"10.1109\/43.298033"},{"key":"25_CR45","unstructured":"Meel, K.S., Yang, S., Liang, V.: INC: a scalable incremental weighted sampler. In: FMCAD 2022, vol.\u00a03, p. 205. TU Wien Academic Press (2022)"},{"key":"25_CR46","unstructured":"Mei, J.: The Quokka# repository. https:\/\/github.com\/System-Verification-Lab\/Quokka-Sharp. Accessed 29 Mar 2024"},{"key":"25_CR47","doi-asserted-by":"crossref","unstructured":"Mei, J., Bonsangue, M., Laarman, A.: Simulating quantum circuits by model counting. arXiv:2403.07197 (2024)","DOI":"10.1007\/978-3-031-63501-4_21"},{"key":"25_CR48","doi-asserted-by":"crossref","unstructured":"Mei, J., Coopmans, T., Bonsangue, M., Laarman, A.: Equivalence checking of quantum circuits by model counting. In: IJCAR (accepted for publication), Pre-print available at arXiv:2403.18813 (2024)","DOI":"10.1007\/978-3-031-63501-4_21"},{"key":"25_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-319-99498-7_12","volume-title":"Reversible Computation","author":"G Meuli","year":"2018","unstructured":"Meuli, G., Soeken, M., De Micheli, G.: SAT-based CNOT, T quantum circuit synthesis. In: Kari, J., Ulidowski, I. (eds.) RC 2018. LNCS, vol. 11106, pp. 175\u2013188. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99498-7_12"},{"key":"25_CR50","doi-asserted-by":"crossref","unstructured":"Miller, D.M., Thornton, M.A.: QMDD: a decision diagram structure for reversible and quantum circuits. In: 36th International Symposium on Multiple-Valued Logic (ISMVL\u201906), pp. 30\u201330. IEEE (2006)","DOI":"10.1109\/ISMVL.2006.35"},{"issue":"1","key":"25_CR51","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1038\/s41534-020-0257-5","volume":"6","author":"Y Nam","year":"2020","unstructured":"Nam, Y., Su, Y., Maslov, D.: Approximate quantum fourier transform with $$o(n \\log (n))$$ t gates. NPJ Quantum Inf. 6(1), 26 (2020)","journal-title":"NPJ Quantum Inf."},{"key":"25_CR52","unstructured":"Nielsen, M.A., Chuang, I.L.: Quantum Information and Quantum Computation. Cambridge University Press, Cambridge, vol. 2, issue 8, p. 23 (2000)"},{"issue":"12","key":"25_CR53","doi-asserted-by":"publisher","first-page":"4657","DOI":"10.1109\/TCAD.2020.2977603","volume":"39","author":"P Niemann","year":"2020","unstructured":"Niemann, P., Zulehner, A., Drechsler, R., Wille, R.: Overcoming the tradeoff between accuracy and compactness in decision diagrams for quantum computation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 39(12), 4657\u20134668 (2020)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"25_CR54","unstructured":"Oztok, U., Darwiche, A.: A top-down compiler for sentential decision diagrams. In: IJCAI\u201915, pp. 3141\u20133148. AAAI Press (2015)"},{"key":"25_CR55","doi-asserted-by":"publisher","first-page":"223","DOI":"10.22331\/q-2020-01-13-223","volume":"4","author":"H Pashayan","year":"2020","unstructured":"Pashayan, H., Bartlett, S.D., Gross, D.: From estimation of quantum probabilities to simulation of quantum circuits. Quantum 4, 223 (2020)","journal-title":"Quantum"},{"issue":"3","key":"25_CR56","doi-asserted-by":"publisher","first-page":"662","DOI":"10.1109\/JETCAS.2022.3202204","volume":"12","author":"T Peham","year":"2022","unstructured":"Peham, T., Burgholzer, L., Wille, R.: Equivalence checking of quantum circuits with the ZX-calculus. IEEE J. Emerging Sel. Top. Circ. Syst. 12(3), 662\u2013675 (2022)","journal-title":"IEEE J. Emerging Sel. Top. Circ. Syst."},{"key":"25_CR57","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.108.012403","volume":"108","author":"S Polla","year":"2023","unstructured":"Polla, S., Anselmetti, G.-L.R., O\u2019Brien, T.E.: Optimizing the information extracted by a single qubit measurement. Phys. Rev. A 108, 012403 (2023)","journal-title":"Phys. Rev. A"},{"key":"25_CR58","doi-asserted-by":"publisher","first-page":"1062","DOI":"10.22331\/q-2023-07-20-1062","volume":"7","author":"N Quetschlich","year":"2023","unstructured":"Quetschlich, N., Burgholzer, L., Wille, R.: MQT bench: benchmarking software and design automation tools for quantum computing. Quantum 7, 1062 (2023)","journal-title":"Quantum"},{"key":"25_CR59","doi-asserted-by":"publisher","first-page":"5188","DOI":"10.1103\/PhysRevLett.86.5188","volume":"86","author":"R Raussendorf","year":"2001","unstructured":"Raussendorf, R., Briegel, H.J.: A one-way quantum computer. Phys. Rev. Lett. 86, 5188\u20135191 (2001)","journal-title":"Phys. Rev. Lett."},{"key":"25_CR60","unstructured":"Sang, T., Bacchus, F., Beame, P., Kautz, H.A., Pitassi, T.: Combining component caching and clause learning for effective model counting. In: International Conference on Theory and Applications of Satisfiability Testing (2004)"},{"key":"25_CR61","unstructured":"Sanner, S., McAllester, D.: Affine algebraic decision diagrams (AADDs) and their application to structured probabilistic inference. In: Proceedings of the 19th International Joint Conference on Artificial Intelligence, IJCAI\u201905, pp. 1384\u20131390, San Francisco, CA, USA (2005). Morgan Kaufmann Publishers Inc"},{"key":"25_CR62","doi-asserted-by":"crossref","unstructured":"Schneider, S., Burgholzer, L., Wille, R.: A SAT encoding for optimal Clifford circuit synthesis. In: Proceedings of the 28th Asia and South Pacific Design Automation Conference, ASPDAC \u201923. ACM (2023)","DOI":"10.1145\/3566097.3567929"},{"key":"25_CR63","doi-asserted-by":"crossref","unstructured":"Shaik, I., van\u00a0de Pol, J.: Optimal layout synthesis for quantum circuits as classical planning. arXiv preprint arXiv:2304.12014 (2023)","DOI":"10.1109\/ICCAD57390.2023.10323924"},{"key":"25_CR64","doi-asserted-by":"publisher","unstructured":"Sistla, M., Chaudhuri, S., Reps, T.: Symbolic quantum simulation with quasimodo. In: Enea, C., Lal, A., editors, Computer Aided Verification, pp. 213\u2013225. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_11","DOI":"10.1007\/978-3-031-37709-9_11"},{"key":"25_CR65","doi-asserted-by":"crossref","unstructured":"Sistla, M., Chaudhuri, S., Reps, T.: Weighted context-free-language ordered binary decision diagrams. arXiv preprint arXiv:2305.13610 (2023)","DOI":"10.1145\/3651157"},{"key":"25_CR66","doi-asserted-by":"publisher","first-page":"793","DOI":"10.1103\/PhysRevLett.77.793","volume":"77","author":"AM Steane","year":"1996","unstructured":"Steane, A.M.: Error correcting codes in quantum theory. Phys. Rev. Lett. 77, 793\u2013797 (1996)","journal-title":"Phys. Rev. Lett."},{"issue":"2","key":"25_CR67","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1023\/A:1008691605584","volume":"10","author":"P Tafertshofer","year":"1997","unstructured":"Tafertshofer, P., Pedram, M.: Factored edge-valued binary decision diagrams. Formal Methods Syst. Design 10(2), 243\u2013270 (1997)","journal-title":"Formal Methods Syst. Design"},{"key":"25_CR68","doi-asserted-by":"publisher","unstructured":"Thanos, D., Coopmans, T., Laarman, A.: Fast equivalence checking of quantum circuits of Clifford gates. In: Andr\u00e9, \u00c9., Sun, J., eds, Automated Technology for Verification and Analysis, pp. 199\u2013216. Springer Nature Switzerland, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-45332-8_10","DOI":"10.1007\/978-3-031-45332-8_10"},{"key":"25_CR69","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.72.022340","volume":"72","author":"G T\u00f3th","year":"2005","unstructured":"T\u00f3th, G., G\u00fchne, O.: Entanglement detection in the stabilizer formalism. Phys. Rev. A 72, 022340 (2005)","journal-title":"Phys. Rev. A"},{"key":"25_CR70","doi-asserted-by":"crossref","unstructured":"Viamontes, G.F., Markov, I.L., Hayes, J.P.: Improving gate-level simulation of quantum circuits. Quantum Inf. Process. 2(5), 347\u2013380 (2003)","DOI":"10.1023\/B:QINP.0000022725.70000.4a"},{"key":"25_CR71","doi-asserted-by":"crossref","unstructured":"Viamontes, G.F., Markov, I.L., Hayes, J.P.: High-performance QuIDD-based simulation of quantum circuits. In: Proceedings Design, Automation and Test in Europe Conference and Exhibition, vol. 2, pp. 1354\u20131355 (2004)","DOI":"10.1109\/DATE.2004.1269084"},{"issue":"9","key":"25_CR72","doi-asserted-by":"publisher","first-page":"3143","DOI":"10.1109\/TCAD.2021.3117506","volume":"41","author":"Q Wang","year":"2022","unstructured":"Wang, Q., Li, R., Ying, M.: Equivalence checking of sequential quantum circuits. IEEE Trans. Comput. Aided Des. Integr. Circ. Syst. 41(9), 3143\u20133156 (2022)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circ. Syst."},{"key":"25_CR73","doi-asserted-by":"crossref","unstructured":"Wille, R., Zhang, H., Drechsler, R.: ATPG for reversible circuits using simulation, Boolean satisfiability, and pseudo Boolean optimization. In: 2011 IEEE Computer Society Annual Symposium on VLSI, pp. 120\u2013125 (2011)","DOI":"10.1109\/ISVLSI.2011.77"},{"key":"25_CR74","unstructured":"Wilson, N.: Decision diagrams for the computation of semiring valuations. In: Proceedings of the 19th International Joint Conference on Artificial Intelligence, pp. 331\u2013336 (2005)"},{"issue":"1","key":"25_CR75","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1186\/s41313-022-00047-7","volume":"6","author":"J Wright","year":"2022","unstructured":"Wright, J., et al.: Numerical simulations of noisy quantum circuits for computational chemistry. Materials Theory 6(1), 18 (2022)","journal-title":"Materials Theory"},{"key":"25_CR76","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.103.052426","volume":"103","author":"Y Zhang","year":"2021","unstructured":"Zhang, Y., Tang, Y., Zhou, Y., Ma, X.: Efficient entanglement generation and detection of generalized stabilizer states. Phys. Rev. A 103, 052426 (2021)","journal-title":"Phys. Rev. A"},{"issue":"5","key":"25_CR77","first-page":"996","volume":"37","author":"A Zulehner","year":"2018","unstructured":"Zulehner, A., Wille, R.: One-pass design of reversible circuits: combining embedding and synthesis for reversible logic. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 37(5), 996\u20131008 (2018)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65633-0_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,24]],"date-time":"2024-11-24T20:16:07Z","timestamp":1732479367000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65633-0_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656323","9783031656330"],"references-count":77,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65633-0_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}