{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:11:16Z","timestamp":1784837476031,"version":"3.55.0"},"publisher-location":"Cham","reference-count":64,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031635007","type":"print"},{"value":"9783031635014","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,2]],"date-time":"2024-07-02T00:00:00Z","timestamp":1719878400000},"content-version":"vor","delay-in-days":183,"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>Verifying equivalence between two quantum circuits is a hard problem, that is nonetheless crucial in compiling and optimizing quantum algorithms for real-world devices. This paper gives a Turing reduction of the (universal) quantum circuits equivalence problem to weighted model counting (WMC). Our starting point is a folklore theorem showing that equivalence checking of quantum circuits can be done in the so-called Pauli-basis. We combine this insight with a WMC encoding of quantum circuit simulation, which we extend with support for the Toffoli gate. Finally, we prove that the weights computed by the model counter indeed realize the reduction. With an open-source implementation, we demonstrate that this novel approach can outperform a state-of-the-art equivalence-checking tool based on ZX calculus and decision diagrams.<\/jats:p>","DOI":"10.1007\/978-3-031-63501-4_21","type":"book-chapter","created":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T09:02:00Z","timestamp":1719824520000},"page":"401-421","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Equivalence Checking of\u00a0Quantum Circuits by\u00a0Model Counting"],"prefix":"10.1007","author":[{"given":"Jingyi","family":"Mei","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tim","family":"Coopmans","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marcello","family":"Bonsangue","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alfons","family":"Laarman","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,7,2]]},"reference":[{"issue":"5","key":"21_CR1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.70.052328","volume":"70","author":"S Aaronson","year":"2004","unstructured":"Aaronson, S., Gottesman, D.: Improved simulation of stabilizer circuits. Phys. Rev. A 70(5), 052328 (2004)","journal-title":"Phys. Rev. A"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Amy, M.: Towards large-scale functional verification of universal quantum circuits. arXiv:1805.06908 (2018)","DOI":"10.4204\/EPTCS.287.1"},{"key":"21_CR3","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-031-27481-7_12","volume-title":"FM 2023","author":"F Bauer-Marquart","year":"2023","unstructured":"Bauer-Marquart, F., Leue, S., Schilling, C.: symQV: automated symbolic verification of quantum programs. In: Chechik, M., Katoen, J.-P., Leucker, M. (eds.) FM 2023. LNCS, vol. 14000, pp. 181\u2013198. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_12"},{"key":"21_CR4","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: SAT 2022. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"key":"21_CR5","doi-asserted-by":"publisher","first-page":"1185","DOI":"10.22331\/q-2023-11-20-1185","volume":"7","author":"B Bichsel","year":"2023","unstructured":"Bichsel, B., Paradis, A., Baader, M., Vechev, M.: Abstraqt: analysis of quantum circuits via abstract stabilizer simulation. Quantum 7, 1185 (2023)","journal-title":"Quantum"},{"key":"21_CR6","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. In: Handbook of Satisfiability, vol. 185, no. 99, pp. 457\u2013481 (2009)"},{"key":"21_CR7","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009)"},{"issue":"9","key":"21_CR8","doi-asserted-by":"publisher","first-page":"1810","DOI":"10.1109\/TCAD.2020.3032630","volume":"40","author":"L Burgholzer","year":"2021","unstructured":"Burgholzer, L., Wille, R.: Advanced equivalence checking for quantum circuits. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 40(9), 1810\u20131824 (2021)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"Calderbank, A.R., Shor, P.W.: Good quantum error-correcting codes exist. Phys. Rev. A 54, 1098\u20131105 (1996)","DOI":"10.1103\/PhysRevA.54.1098"},{"issue":"6","key":"21_CR10","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":"21_CR11","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-031-38499-8_10","volume-title":"CADE 2023","author":"Y-F Chen","year":"2023","unstructured":"Chen, Y.-F., R\u00fcmmer, P., Tsai, W.-L.: A theory of cartesian arrays (with applications in quantum circuit verification). In: Pientka, B., Tinelli, C. (eds.) CADE 2023. LNCS, pp. 170\u2013189. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_10"},{"issue":"4","key":"21_CR12","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":"21_CR13","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":"21_CR14","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."},{"key":"21_CR15","unstructured":"de\u00a0Beaudrap, N., Kissinger, A., van\u00a0de Wetering, J.: Circuit extraction for ZX-diagrams can be #P-hard. In: ICALP 2022. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"key":"21_CR16","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1007\/978-3-031-37709-9_18","volume-title":"CAV 2023","author":"N Feng","year":"2023","unstructured":"Feng, N., Marsso, L., Sabetzadeh, M., Chechik, M.: Early verification of legal compliance via bounded satisfiability checking. In: Enea, C., Lal, A. (eds.) CAV 2023. LNCS, vol. 13966, pp. 374\u2013396. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_18"},{"issue":"1","key":"21_CR17","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1146\/annurev-conmatphys-031720-030658","volume":"14","author":"MPA Fisher","year":"2023","unstructured":"Fisher, M.P.A., Khemani, V., Nahum, A., Vijay, S.: Random quantum circuits. Annu. Rev. Condens. Matter Phys. 14(1), 335\u2013379 (2023)","journal-title":"Annu. Rev. Condens. Matter Phys."},{"key":"21_CR18","unstructured":"Gay, S.J.: Stabilizer states as a basis for density matrices. CoRR, abs\/1112.2156 (2011)"},{"key":"21_CR19","unstructured":"Gomes, C.P., Sabharwal, A., Selman, B.: Model counting. In: Handbook of Satisfiability, pp. 993\u20131014. IOS Press (2021)"},{"key":"21_CR20","unstructured":"Gottesman, D.: Stabilizer codes and quantum error correction. Ph.D. thesis, California Institute of Technology (1997)"},{"key":"21_CR21","unstructured":"Hecher, M., Fichte, J.K.: Model counting competition 2023. https:\/\/mccompetition.org\/. Accessed 07 Jan 2024"},{"key":"21_CR22","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 2022. Association for Computing Machinery, New York (2022)","DOI":"10.1145\/3508352.3549479"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Hong, X., Ying, M., Feng, Y., Zhou, X., Li, S.: Approximate equivalence checking of noisy quantum circuits. In: 2021 58th ACM\/IEEE Design Automation Conference (DAC), pp. 637\u2013642 (2021)","DOI":"10.1109\/DAC18074.2021.9586214"},{"issue":"03","key":"21_CR24","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1142\/S0219749905001067","volume":"3","author":"D Janzing","year":"2005","unstructured":"Janzing, D., Wocjan, P., Beth, T.: \u201cNon-identity-check\u2019\u2019 is QMA-complete. Int. J. Quantum Inf. 3(03), 463\u2013473 (2005)","journal-title":"Int. J. Quantum Inf."},{"key":"21_CR25","unstructured":"Ji, Z., Wu, X.: Non-identity check remains QMA-complete for short circuits. arXiv:0906.5416 (2009)"},{"key":"21_CR26","doi-asserted-by":"crossref","unstructured":"Jim\u00e9nez-Pastor, A., Larsen, K.G., Tribastone, M., Tschaikowski, M.: Forward and backward constrained bisimulations for quantum circuits (2024)","DOI":"10.1007\/978-3-031-57249-4_17"},{"key":"21_CR27","unstructured":"Jones, T.: Decomposing dense matrices into dense Pauli tensors. arXiv:2401.16378 (2024)"},{"key":"21_CR28","doi-asserted-by":"crossref","unstructured":"Kissinger, A., van\u00a0de Wetering, J.: PyZX: large scale automated diagrammatic reasoning. In: QPL (2019)","DOI":"10.4204\/EPTCS.318.14"},{"issue":"4","key":"21_CR29","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). arXiv:2109.01076 [quant-ph]","journal-title":"Quantum Sci. Technol."},{"issue":"6","key":"21_CR30","doi-asserted-by":"publisher","first-page":"1191","DOI":"10.1070\/RM1997v052n06ABEH002155","volume":"52","author":"AY Kitaev","year":"1997","unstructured":"Kitaev, A.Y.: Quantum computations: algorithms and error correction. Russ. Math. Surv. 52(6), 1191 (1997)","journal-title":"Russ. Math. Surv."},{"key":"21_CR31","doi-asserted-by":"crossref","unstructured":"Kitaev, A.Y., Shen, A., Vyalyi, M.N.: Classical and quantum computation. American Mathematical Society (2002)","DOI":"10.1090\/gsm\/047"},{"key":"21_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/11830924_40","volume-title":"Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques","author":"Y-K Liu","year":"2006","unstructured":"Liu, Y.-K.: Consistency of local density matrices is QMA-complete. In: D\u00edaz, J., Jansen, K., Rolim, J.D.P., Zwick, U. (eds.) APPROX\/RANDOM -2006. LNCS, vol. 4110, pp. 438\u2013449. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11830924_40"},{"issue":"6","key":"21_CR33","doi-asserted-by":"publisher","first-page":"1417","DOI":"10.1002\/j.1538-7305.1956.tb03835.x","volume":"35","author":"EJ McCluskey","year":"1956","unstructured":"McCluskey, E.J.: Minimization of boolean functions. Bell Syst. Tech. J. 35(6), 1417\u20131444 (1956)","journal-title":"Bell Syst. Tech. J."},{"key":"21_CR34","doi-asserted-by":"crossref","unstructured":"Mei, J., Bonsangue, M., Laarman, A.: Simulating quantum circuits by model counting. In: CAV 2024. Springer, Cham (2024, accepted for publication). Pre-print available at arXiv:2403.07197","DOI":"10.1007\/978-3-031-65633-0_25"},{"key":"21_CR35","doi-asserted-by":"crossref","unstructured":"Mei, J., Coopmans, T., Bonsangue, M., Laarman, A.: Equivalence checking of quantum circuits by model counting. arXiv preprint arXiv:2403.18813 (2024)","DOI":"10.1007\/978-3-031-63501-4_21"},{"key":"21_CR36","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":"21_CR37","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 2006), pp. 30\u201330 (2006)","DOI":"10.1109\/ISMVL.2006.35"},{"key":"21_CR38","unstructured":"Nielsen, M.A., Chuang, I.L.: Quantum Information and Quantum Computation, vol. 2, no. 8, p. 23. Cambridge University Press, Cambridge (2000)"},{"issue":"12","key":"21_CR39","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":"21_CR40","unstructured":"Oztok, U., Darwiche, A.: A top-down compiler for sentential decision diagrams. In: SEA 2020, IJCAI 2015, pp. 3141\u20133148. AAAI Press (2015)"},{"issue":"3","key":"21_CR41","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. Emerg. Sel. Top. Circ. Syst. 12(3), 662\u2013675 (2022)","journal-title":"IEEE J. Emerg. Sel. Top. Circ. Syst."},{"key":"21_CR42","doi-asserted-by":"crossref","unstructured":"Peham, T., Burgholzer, L., Wille, R.: Equivalence checking of parameterized quantum circuits: verifying the compilation of variational quantum algorithms. In: 2023 28th Asia and South Pacific Design Automation Conference (ASP-DAC), pp. 702\u2013708 (2023)","DOI":"10.1145\/3566097.3567932"},{"key":"21_CR43","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"},{"issue":"8","key":"21_CR44","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1080\/00029890.1952.11988183","volume":"59","author":"WV Quine","year":"1952","unstructured":"Quine, W.V.: The problem of simplifying truth functions. Am. Math. Mon. 59(8), 521\u2013531 (1952)","journal-title":"Am. Math. Mon."},{"key":"21_CR45","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-031-38100-3_10","volume-title":"RC 2023","author":"A-J Quist","year":"2023","unstructured":"Quist, A.-J., Laarman, A.: Optimizing quantum space using spooky pebble games. In: Kutrib, M., Meyer, U. (eds.) RC 2023. LNCS, vol. 13960, pp. 134\u2013149. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-38100-3_10"},{"key":"21_CR46","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":"21_CR47","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)"},{"issue":"4","key":"21_CR48","doi-asserted-by":"publisher","first-page":"R2493","DOI":"10.1103\/PhysRevA.52.R2493","volume":"52","author":"PW Shor","year":"1995","unstructured":"Shor, P.W.: Scheme for reducing decoherence in quantum computer memory. Phys. Rev. A 52(4), R2493 (1995)","journal-title":"Phys. Rev. A"},{"issue":"5","key":"21_CR49","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(5), 793 (1996)","journal-title":"Phys. Rev. Lett."},{"key":"21_CR50","unstructured":"Suzuki, R., Hashimoto, K., Sakai, M.: Improvement of projected model-counting solver with component decomposition using SAT solving in components. Technical report, JSAI Technical Report, SIG-FPAI-103-B506 (2017). (in Japanese)"},{"issue":"05","key":"21_CR51","doi-asserted-by":"publisher","first-page":"807","DOI":"10.1142\/S0219749910006599","volume":"8","author":"Yu Tanaka","year":"2010","unstructured":"Tanaka, Yu.: Exact non-identity check is NQP-complete. Int. J. Quantum Inf. 8(05), 807\u2013819 (2010)","journal-title":"Int. J. Quantum Inf."},{"key":"21_CR52","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-031-45332-8_10","volume-title":"ATVA 2023","author":"D Thanos","year":"2023","unstructured":"Thanos, D., Coopmans, T., Laarman, A.: Fast equivalence checking of quantum circuits of Clifford gates. In: Andr\u00e9, \u00c9., Sun, J. (eds.) ATVA 2023. LNCS, vol. 14216, pp. 199\u2013216. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-45332-8_10"},{"key":"21_CR53","doi-asserted-by":"crossref","unstructured":"Thanos, D., et al.: Automated reasoning in quantum circuit compilation. In: Model Checking Software (SPIN) 2024. Springer, Cham (2024, accepted for publication)","DOI":"10.1007\/978-3-031-66149-5_6"},{"issue":"3","key":"21_CR54","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":"21_CR55","doi-asserted-by":"crossref","unstructured":"Viamontes, G.F., Markov, I.L., Hayes, J.P.: Checking equivalence of quantum circuits and states. In: 2007 IEEE\/ACM International Conference on Computer-Aided Design, pp. 69\u201374 (2007)","DOI":"10.1109\/ICCAD.2007.4397246"},{"issue":"2","key":"21_CR56","doi-asserted-by":"publisher","first-page":"584","DOI":"10.1093\/ietfec\/e91-a.2.584","volume":"91","author":"S-A Wang","year":"2008","unstructured":"Wang, S.-A., Lu, C.-Y., Tsai, I.-M., Kuo, S.-Y.: An XQDD-based verification method for quantum circuits. IEICE Trans. Fundam. Electron. Commun. Comput. Sci. 91(2), 584\u2013594 (2008)","journal-title":"IEICE Trans. Fundam. Electron. Commun. Comput. Sci."},{"key":"21_CR57","doi-asserted-by":"crossref","unstructured":"Wei, C.-Y., Tsai, Y.-H., Jhang, C.-S., Jiang, J.-H.R.: Accurate BDD-based unitary operator manipulation for scalable and robust quantum circuit verification. In: Proceedings of the 59th ACM\/IEEE Design Automation Conference, pp. 523\u2013528 (2022)","DOI":"10.1145\/3489517.3530481"},{"key":"21_CR58","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"},{"issue":"1","key":"21_CR59","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. Mater. Theory 6(1), 18 (2022)","journal-title":"Mater. Theory"},{"key":"21_CR60","first-page":"53","volume":"4","author":"X Lin","year":"2009","unstructured":"Lin, X., Hutter, F., Hoos, H., Leyton-Brown, K.: SATzilla2009: an automatic algorithm portfolio for SAT. SAT 4, 53\u201355 (2009)","journal-title":"SAT"},{"key":"21_CR61","doi-asserted-by":"crossref","unstructured":"Yamashita, S., Markov, I.L.: Fast equivalence-checking for quantum circuits. In: 2010 IEEE\/ACM International Symposium on Nanoscale Architectures, pp. 23\u201328. IEEE (2010)","DOI":"10.1109\/NANOARCH.2010.5510932"},{"key":"21_CR62","doi-asserted-by":"crossref","unstructured":"Yu, N., Palsberg, J.: Quantum abstract interpretation. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 542\u2013558 (2021)","DOI":"10.1145\/3453483.3454061"},{"key":"21_CR63","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"},{"key":"21_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/978-3-319-59936-6_18","volume-title":"Reversible Computation","author":"A Zulehner","year":"2017","unstructured":"Zulehner, A., Wille, R.: Improving synthesis of reversible circuits: exploiting redundancies in paths and nodes of QMDDs. In: Phillips, I., Rahaman, H. (eds.) RC 2017. LNCS, vol. 10301, pp. 232\u2013247. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-59936-6_18"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-63501-4_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,23]],"date-time":"2024-11-23T04:39:35Z","timestamp":1732336775000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63501-4_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031635007","9783031635014"],"references-count":64,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63501-4_21","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":"2 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nancy","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","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":"3 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/merz.gitlabpages.inria.fr\/2024-ijcar\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}