{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:18:12Z","timestamp":1742912292211,"version":"3.40.3"},"publisher-location":"Cham","reference-count":199,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031661488"},{"type":"electronic","value":"9783031661495"}],"license":[{"start":{"date-parts":[[2024,10,13]],"date-time":"2024-10-13T00:00:00Z","timestamp":1728777600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,13]],"date-time":"2024-10-13T00:00:00Z","timestamp":1728777600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-66149-5_6","type":"book-chapter","created":{"date-parts":[[2024,10,12]],"date-time":"2024-10-12T07:01:54Z","timestamp":1728716514000},"page":"106-134","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Automated Reasoning in\u00a0Quantum Circuit Compilation"],"prefix":"10.1007","author":[{"given":"Dimitrios","family":"Thanos","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alejandro","family":"Villoria","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sebastiaan","family":"Brand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arend-Jan","family":"Quist","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jingyi","family":"Mei","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tim","family":"Coopmans","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alfons","family":"Laarman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,10,13]]},"reference":[{"key":"6_CR1","doi-asserted-by":"publisher","unstructured":"Aaronson, S., Gottesman, D.: Improved simulation of stabilizer circuits. Phys. Rev. A 70(5) (2004). https:\/\/doi.org\/10.1103\/PhysRevA.70.052328","DOI":"10.1103\/PhysRevA.70.052328"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Abdollahi, A., Pedram, M.: Analysis and synthesis of quantum circuits by using quantum decision diagrams. In: Proceedings of the Design Automation and Test in Europe Conference, vol.\u00a01, pp. 1\u20136. IEEE (2006)","DOI":"10.1109\/DATE.2006.244176"},{"key":"6_CR3","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":"6_CR4","doi-asserted-by":"crossref","unstructured":"Amy, M.: Towards large-scale functional verification of universal quantum circuits. arXiv preprint arXiv:1805.06908 (2018)","DOI":"10.4204\/EPTCS.287.1"},{"key":"6_CR5","unstructured":"Amy, M.: Formal methods in quantum circuit design (PhD thesis). Ph.D. thesis, University of Waterloo (2019)"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Arute, F., et al.: Quantum supremacy using a programmable superconducting processor. Nature 574(7779), 505\u2013510 (2019)","DOI":"10.1038\/s41586-019-1666-5"},{"key":"6_CR7","doi-asserted-by":"publisher","unstructured":"Backens, M., Kissinger, A.: ZH: A complete graphical calculus for quantum computations involving classical non-linearity. Electron. Proc. Theor. Comput. Sci. 287, 23\u201342 (2019). https:\/\/doi.org\/10.4204\/EPTCS.287.2","DOI":"10.4204\/EPTCS.287.2"},{"key":"6_CR8","doi-asserted-by":"publisher","unstructured":"Backens, M., Miller-Bakewell, H., de\u00a0Felice, G., Lobski, L., van\u00a0de Wetering, J.: There and back again: a circuit extraction tale. Quantum 5, 421 (2021). https:\/\/doi.org\/10.22331\/q-2021-03-25-421","DOI":"10.22331\/q-2021-03-25-421"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Bahar, R.I., et al.: Algebraic decision diagrams and their applications. Formal Methods Syst. Des. 10(2\u20133), 171\u2013206 (1997)","DOI":"10.1023\/A:1008699807402"},{"key":"6_CR10","doi-asserted-by":"publisher","unstructured":"Barends, R., et al.: Superconducting quantum circuits at the surface code threshold for fault tolerance. Nature 508(7497), 500\u2013503 (2014). https:\/\/doi.org\/10.1038\/nature13171","DOI":"10.1038\/nature13171"},{"key":"6_CR11","doi-asserted-by":"publisher","unstructured":"Ba\u00dfler, P., et al.: Synthesis of and compilation with time-optimal multi-qubit gates. Quantum 7, 984 (2023). https:\/\/doi.org\/10.22331\/q-2023-04-20-984","DOI":"10.22331\/q-2023-04-20-984"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Bauer-Marquart, F., Leue, S., Schilling, C.: symQV: automated symbolic verification of quantum programs. In: Formal Methods: 25th International Symposium, FM 2023, L\u00fcbeck, 6\u201310 March 2023, Proceedings, pp. 181\u2013198. Springer, Heidelberg (2023)","DOI":"10.1007\/978-3-031-27481-7_12"},{"key":"6_CR13","unstructured":"de\u00a0Beaudrap, N., Bian, X., Wang, Q.: Fast and effective techniques for T-count reduction via spider nest identities. In: Flammia, S.T. (ed.) 15th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol. 158, pp. 11:1\u201311:23. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2020). https:\/\/drops-dev.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.TQC.2020.11"},{"key":"6_CR14","unstructured":"de\u00a0Beaudrap, N., Kissinger, A., van\u00a0de Wetering, J.: Circuit extraction for ZX-diagrams can be #P-hard. In: Boja\u0144czyk, M., Merelli, E., Woodruff, D.P. (eds.) 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.ICALP.2022.119"},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Benedetti, M., Lloyd, E., Sack, S., Fiorentini, M.: Parameterized quantum circuits as machine learning models. Quant. Sci. Technol. 4(4), 043001 (2019). https:\/\/doi.org\/10.1088\/2058-9565\/ab4eb5","DOI":"10.1088\/2058-9565\/ab4eb5"},{"key":"6_CR16","doi-asserted-by":"publisher","unstructured":"Berent, L., Burgholzer, L., Derks, P.J.H., Eisert, J., Wille, R.: Decoding quantum color codes with MaxSAT. arXiv preprint arXiv:2303.14237 (2023). https:\/\/doi.org\/10.48550\/arXiv.2303.14237","DOI":"10.48550\/arXiv.2303.14237"},{"key":"6_CR17","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. (eds.) 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 236, pp. 18:1\u201318:17. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2022). https:\/\/drops-dev.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.SAT.2022.18"},{"issue":"24","key":"6_CR18","doi-asserted-by":"publisher","DOI":"10.1088\/1751-8113\/44\/24\/245304","volume":"44","author":"V Bergholm","year":"2011","unstructured":"Bergholm, V., Biamonte, J.D.: Categorical quantum circuits. J. Phys. A: Math. Theor. 44(24), 245304 (2011)","journal-title":"J. Phys. A: Math. Theor."},{"key":"6_CR19","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2013)"},{"key":"6_CR20","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Handb. Satisfiabil. 185(99), 457\u2013481 (2009)"},{"key":"6_CR21","unstructured":"Biere, A., Heule, M., van Maaren, H.: Handbook of Satisfiability, vol. 185. IOS Press (2009)"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Boole, G.: An investigation of the laws of thought, on which are founded the mathematical theories of logic and probabilities. Walton and Maberly (1854)","DOI":"10.5962\/bhl.title.29413"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Borgna, A., Perdrix, S., Valiron, B.: Hybrid quantum-classical circuit simplification with the zx-calculus. In: Oh, H. (ed.) Programming Languages and Systems, pp. 121\u2013139. Springer, Cham (2021)","DOI":"10.1007\/978-3-030-89051-3_8"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Bove, A., Dybjer, P., Norell, U.: A brief overview of Agda \u2013 a functional language with dependent types. In: Theorem Proving in Higher Order Logics: 22nd International Conference, TPHOLs 2009, Munich, 17\u201320 August 2009. Proceedings 22, pp. 73\u201378. Springer, Cham (2009)","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Brand, S., B\u00e4ck, T., Laarman, A.: A decision diagram operation for reachability. In: International Symposium on Formal Methods, pp. 514\u2013532. Springer, Cham (2023)","DOI":"10.1007\/978-3-031-27481-7_29"},{"key":"6_CR26","unstructured":"Brand, S., Coopmans, T., Laarman, A.: Quantum graph-state synthesis with SAT. Proceedings of the 14th International Workshop on Pragmatics of SAT (2023)"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Brandhofer, S., Kim, J., Niu, S., Bronn, N.T.: SAT-based quantum circuit adaptation. In: 2023 Design, Automation and Test in Europe Conference and Exhibition (DATE), pp. 1\u20136. IEEE (2023)","DOI":"10.23919\/DATE56975.2023.10137140"},{"key":"6_CR28","doi-asserted-by":"publisher","unstructured":"Bravyi, S., Browne, D., Calpin, P., Campbell, E., Gosset, D., Howard, M.: Simulation of quantum circuits by low-rank stabilizer decompositions. Quantum 3, 181 (2019). https:\/\/doi.org\/10.22331\/q-2019-09-02-181","DOI":"10.22331\/q-2019-09-02-181"},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293\u2013318 (1992)","DOI":"10.1145\/136035.136043"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"Burgholzer, L., Bauer, H., Wille, R.: Hybrid Schr\u00f6dinger-Feynman simulation of quantum circuits with decision diagrams. In: 2021 IEEE International Conference on Quantum Computing and Engineering (QCE), pp. 199\u2013206 (2021)","DOI":"10.1109\/QCE52317.2021.00037"},{"key":"6_CR31","doi-asserted-by":"crossref","unstructured":"Burgholzer, L., Kueng, R., Wille, R.: Random stimuli generation for the verification of quantum circuits. In: Proceedings of the 26th Asia and South Pacific Design Automation Conference, pp. 767\u2013772 (2021)","DOI":"10.1145\/3394885.3431590"},{"key":"6_CR32","doi-asserted-by":"crossref","unstructured":"Burgholzer, L., Wille, R.: Advanced equivalence checking for quantum circuits. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 40(9), 1810\u20131824 (2020)","DOI":"10.1109\/TCAD.2020.3032630"},{"key":"6_CR33","doi-asserted-by":"crossref","unstructured":"Burgholzer, L., Wille, R.: Improved DD-based equivalence checking of quantum circuits. In: 25th Asia and South Pacific Design Automation Conference (ASP-DAC), pp. 127\u2013132 (2020)","DOI":"10.1109\/ASP-DAC47756.2020.9045153"},{"key":"6_CR34","doi-asserted-by":"publisher","DOI":"10.1016\/j.simpa.2020.100051","volume":"7","author":"L Burgholzer","year":"2021","unstructured":"Burgholzer, L., Wille, R.: QCEC: A JKQ tool for quantum circuit equivalence checking. Software Impacts 7, 100051 (2021)","journal-title":"Software Impacts"},{"key":"6_CR35","unstructured":"Cam, T., Martiel, S.: Speeding up quantum circuits simulation using ZX-calculus. arXiv preprint arXiv:2305.02669 (2023)"},{"key":"6_CR36","doi-asserted-by":"publisher","unstructured":"Carette, T., Jeandel, E., Perdrix, S., Vilmart, R.: Completeness of graphical languages for mixed state quantum mechanics. ACM Trans. Quant. Comput. 2(4), 1\u201328 (2021). https:\/\/doi.org\/10.1145\/3464693","DOI":"10.1145\/3464693"},{"key":"6_CR37","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"},{"key":"6_CR38","unstructured":"Chareton, C., Bardin, S., Lee, D., Valiron, B., Vilmart, R., Xu, Z.: Formal methods for quantum programs: a survey. arXiv preprint arXiv:2109.06493 (2021)"},{"key":"6_CR39","doi-asserted-by":"publisher","unstructured":"Chen, Y.-F., R\u00fcmmer, P., Tsai, W.-L.: A theory of\u00a0Cartesian arrays (with applications in\u00a0quantum circuit verification). In: Pientka, B., Tinelli, C. (eds.) CADE 29, pp. 170\u2013189. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_10","DOI":"10.1007\/978-3-031-38499-8_10"},{"key":"6_CR40","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"},{"key":"6_CR41","unstructured":"Cl\u00e9ment, A., Delorme, N., Perdrix, S., Vilmart, R.: Quantum circuit completeness: extensions and simplifications. In: Murano, A., Silva, A. (eds.) 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), vol. 288, pp. 20:1\u201320:23. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2024). https:\/\/drops-dev.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.CSL.2024.20"},{"key":"6_CR42","doi-asserted-by":"crossref","unstructured":"Cl\u00e9ment, A., Heurtel, N., Mansfield, S., Perdrix, S., Valiron, B.: LOv-calculus: a graphical language for linear optical quantum circuits. In: Szeider, S., Ganian, R., Silva, A. (eds.) 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 241, pp. 35:1\u201335:16. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2022). https:\/\/drops-dev.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.MFCS.2022.35","DOI":"10.1109\/QCE53715.2022.00080"},{"key":"6_CR43","doi-asserted-by":"crossref","unstructured":"Coecke, B., Duncan, R.: Interacting quantum observables: categorical algebra and diagrammatics. New J. Phys. 13(4), 043016 (2011). arXiv:0906.4725 [quant-ph]","DOI":"10.1088\/1367-2630\/13\/4\/043016"},{"key":"6_CR44","doi-asserted-by":"crossref","unstructured":"Coecke, B., Kissinger, A.: Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning. Cambridge University Press (2017)","DOI":"10.1017\/9781316219317"},{"key":"6_CR45","doi-asserted-by":"publisher","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the Third Annual ACM Symposium on Theory of Computing (STOC 1971), pp. 151\u2013158. Association for Computing Machinery, New York (1971). https:\/\/doi.org\/10.1145\/800157.805047","DOI":"10.1145\/800157.805047"},{"key":"6_CR46","unstructured":"C\u00f3rcoles, A.D., et al.: Challenges and opportunities of near-term quantum computing systems. arXiv preprint arXiv:1910.02894 (2019)"},{"key":"6_CR47","doi-asserted-by":"publisher","unstructured":"Cowtan, A., Dilkes, S., Duncan, R., Simmons, W., Sivarajah, S.: Phase gadget synthesis for shallow circuits. Electron. Proc. Theor. Comput. Sci. 318, 213\u2013228 (2020). https:\/\/doi.org\/10.4204\/EPTCS.318.13","DOI":"10.4204\/EPTCS.318.13"},{"key":"6_CR48","unstructured":"Cowtan, A., Simmons, W., Duncan, R.: A generic compilation strategy for the unitary coupled cluster ansatz. arXiv preprint arXiv:2007.10515 (2020)"},{"issue":"4","key":"6_CR49","doi-asserted-by":"publisher","DOI":"10.1088\/2058-9565\/aba763","volume":"5","author":"A Dahlberg","year":"2020","unstructured":"Dahlberg, A., Helsen, J., Wehner, S.: How to transform graph states using single-qubit operations: computational complexity and algorithms. Quant. Sci. Technol. 5(4), 045016 (2020)","journal-title":"Quant. Sci. Technol."},{"issue":"2123","key":"6_CR50","doi-asserted-by":"publisher","first-page":"20170325","DOI":"10.1098\/rsta.2017.0325","volume":"376","author":"A Dahlberg","year":"2018","unstructured":"Dahlberg, A., Wehner, S.: Transforming graph states using single-qubit operations. Philos. Trans. Roy. Soc. A: Math. Phys. Eng. Sci. 376(2123), 20170325 (2018)","journal-title":"Philos. Trans. Roy. Soc. A: Math. Phys. Eng. Sci."},{"key":"6_CR51","unstructured":"Darwiche, A.: SDD: a new canonical representation of propositional knowledge bases. In: Twenty-Second International Joint Conference on Artificial Intelligence (2011)"},{"key":"6_CR52","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1613\/jair.989","volume":"17","author":"A Darwiche","year":"2002","unstructured":"Darwiche, A., Marquis, P.: A knowledge compilation map. J. Artif. Intell. Res. 17, 229\u2013264 (2002)","journal-title":"J. Artif. Intell. Res."},{"issue":"7","key":"6_CR53","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"6_CR54","unstructured":"De\u00a0Felice, G., Hadzihasanovic, A., Ng, K.F.: A diagrammatic calculus of fermionic quantum circuits. Logic. Methods Comput. Sci. 15 (2019)"},{"key":"6_CR55","doi-asserted-by":"publisher","unstructured":"Deng, H., Tao, R., Peng, Y., Wu, X.: A case for synthesis of recursive quantum unitary programs. Proc. ACM Program. Lang. 8(POPL), 1759\u20131788 (2024). https:\/\/doi.org\/10.1145\/3632901","DOI":"10.1145\/3632901"},{"key":"6_CR56","first-page":"127","volume":"296","author":"T van Dijk","year":"2013","unstructured":"van Dijk, T., Laarman, A., van de Pol, J.: Multi-core BDD operations for symbolic reachability. ENTCS 296, 127\u2013143 (2013)","journal-title":"ENTCS"},{"key":"6_CR57","doi-asserted-by":"crossref","unstructured":"Ding, J., Yamashita, S.: Exact synthesis of nearest neighbor compliant quantum circuits in 2-D architecture and its application to large-scale circuits. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 39(5), 1045\u20131058 (2019)","DOI":"10.1109\/TCAD.2019.2907919"},{"key":"6_CR58","doi-asserted-by":"publisher","unstructured":"Ding, Y., Chong, F.T.: Circuit synthesis and compilation. In: Ding, Y., Chong, F.T. (eds.) Quantum Computer Systems: Research for Noisy Intermediate-Scale Quantum Computers, pp. 91\u2013125. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-031-01765-0_6","DOI":"10.1007\/978-3-031-01765-0_6"},{"key":"6_CR59","doi-asserted-by":"publisher","unstructured":"Duncan, R., Kissinger, A., Perdrix, S., van\u00a0de Wetering, J.: Graph-theoretic simplification of quantum circuits with the ZX-calculus. Quantum 4, 279 (2020). https:\/\/doi.org\/10.22331\/q-2020-06-04-279","DOI":"10.22331\/q-2020-06-04-279"},{"key":"6_CR60","doi-asserted-by":"publisher","unstructured":"Duncan, R., Perdrix, S.: Rewriting measurement-based quantum computations with generalised flow. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf\u00a0der Heide, F., Spirakis, P.G. (eds.) Automata, Languages and Programming, pp. 285\u2013296. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14162-1_24","DOI":"10.1007\/978-3-642-14162-1_24"},{"key":"6_CR61","doi-asserted-by":"crossref","unstructured":"Dunjko, V., Briegel, H.J.: Machine learning and artificial intelligence in the quantum domain (2017)","DOI":"10.1088\/1361-6633\/aab406"},{"key":"6_CR62","unstructured":"Fargier, H., Marquis, P., Schmidt, N.: Semiring labelled decision diagrams, revisited: canonicity and spatial efficiency issues. In: IJCAI, pp. 884\u2013890 (2013)"},{"key":"6_CR63","doi-asserted-by":"crossref","unstructured":"Feigenbaum, J., Kannan, S., Vardi, M.Y., Viswanathan, M.: Complexity of problems on graphs represented as OBDDs. In: STACS, pp. 216\u2013226. Springer, Heidelberg (1998)","DOI":"10.1007\/BFb0028563"},{"key":"6_CR64","doi-asserted-by":"publisher","unstructured":"de Felice, G., Coecke, B.: Quantum linear optics via string diagrams. Electron. Proc. Theor. Comput. Sci. 394, 83\u2013100 (2023). https:\/\/doi.org\/10.4204\/EPTCS.394.6","DOI":"10.4204\/EPTCS.394.6"},{"key":"6_CR65","unstructured":"Finigan, W., Cubeddu, M., Lively, T., Flick, J., Narang, P.: Qubit allocation for noisy intermediate-scale quantum computers. arXiv prepirnt arXiv:1810.08291 (2018)"},{"key":"6_CR66","doi-asserted-by":"crossref","unstructured":"Fujita, M., McGeer, P.C., Yang, J.Y.: Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. FMSD 10(2\u20133), 149\u2013169 (1997)","DOI":"10.1023\/A:1008647823331"},{"issue":"3","key":"6_CR67","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.87.032332","volume":"87","author":"B Giles","year":"2013","unstructured":"Giles, B., Selinger, P.: Exact synthesis of multiqubit Clifford+T circuits. Phys. Rev. A 87(3), 032332 (2013)","journal-title":"Phys. Rev. A"},{"key":"6_CR68","doi-asserted-by":"publisher","unstructured":"Gogioso, S., Yeung, R.: Annealing optimisation of mixed ZX phase circuits. Electron. Proc. Theor. Comput. Sci. 394, 415\u2013431 (2023). https:\/\/doi.org\/10.4204\/EPTCS.394.20","DOI":"10.4204\/EPTCS.394.20"},{"key":"6_CR69","unstructured":"Gottesman, D.: Stabilizer codes and quantum error correction. arXiv preprint arXiv:quant-ph\/9705052 (1997)"},{"key":"6_CR70","doi-asserted-by":"publisher","unstructured":"Meijer-van de Griend, A., Duncan, R.: Architecture-aware synthesis of phase polynomials for NISQ devices. Electron. Proce. Theor. Comput. Sci. 394, 116\u2013140 (2023). https:\/\/doi.org\/10.4204\/EPTCS.394.8","DOI":"10.4204\/EPTCS.394.8"},{"key":"6_CR71","doi-asserted-by":"crossref","unstructured":"Grover, L.K.: A fast quantum mechanical algorithm for database search. In: Proceedings of the Twenty-Eighth Annual ACM Symposium on Theory of Computing, pp. 212\u2013219 (1996)","DOI":"10.1145\/237814.237866"},{"key":"6_CR72","doi-asserted-by":"crossref","unstructured":"Grurl, T., Fu\u00df, J., Wille, R.: Considering decoherence errors in the simulation of quantum circuits using decision diagrams. In: Proceedings of the 39th International Conference on Computer-Aided Design, pp. 1\u20137 (2020)","DOI":"10.1145\/3400302.3415622"},{"key":"6_CR73","doi-asserted-by":"crossref","unstructured":"Grurl, T., Fu\u00df, J., Wille, R.: Noise-aware quantum circuit simulation with decision diagrams. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 42(3), 860\u2013873 (2022)","DOI":"10.1109\/TCAD.2022.3182628"},{"key":"6_CR74","doi-asserted-by":"crossref","unstructured":"Grurl, T., Kueng, R., Fu\u00df, J., Wille, R.: Stochastic quantum circuit simulation using decision diagrams. In: 2021 Design, Automation and Test in Europe Conference and Exhibition (DATE), pp. 194\u2013199. IEEE (2021)","DOI":"10.23919\/DATE51398.2021.9474135"},{"key":"6_CR75","doi-asserted-by":"publisher","unstructured":"Guo, Z.H., Wang, T.C.: SMT-based layout synthesis approaches for quantum circuits. In: Proceedings of the 2024 International Symposium on Physical Design (ISPD 2024), pp. 235\u2013243. Association for Computing Machinery, New York (2024). https:\/\/doi.org\/10.1145\/3626184.3633316","DOI":"10.1145\/3626184.3633316"},{"key":"6_CR76","doi-asserted-by":"crossref","unstructured":"Hadzihasanovic, A.: A diagrammatic axiomatisation for qubit entanglement (2015)","DOI":"10.1109\/LICS.2015.59"},{"key":"6_CR77","doi-asserted-by":"crossref","unstructured":"Hahn, F., Pappa, A., Eisert, J.: Quantum network routing and local complementation. NPJ Quant. Inf. 5(1), 76 (2019)","DOI":"10.1038\/s41534-019-0191-6"},{"key":"6_CR78","unstructured":"Hein, M., D\u00fcr, W., Eisert, J., Raussendorf, R., Nest, M., Briegel, H.J.: Entanglement in graph states and its applications. arXiv preprint arXiv:quant-ph\/0602096 (2006)"},{"key":"6_CR79","unstructured":"Heurtel, N.: A complete graphical language for linear optical circuits with finite-photon-number sources and detectors (2024)"},{"key":"6_CR80","doi-asserted-by":"crossref","unstructured":"Hillmich, S., Hadfield, C., Raymond, R., Mezzacapo, A., Wille, R.: Decision diagrams for quantum measurements with shallow circuits. In: 2021 IEEE International Conference on Quantum Computing and Engineering (QCE), pp. 24\u201334. IEEE (2021)","DOI":"10.1109\/QCE52317.2021.00018"},{"key":"6_CR81","unstructured":"Holker, C.: Causal flow preserving optimisation of quantum circuits in the ZX-calculus. arXiv preprint arXiv:2312.02793 (2023)"},{"key":"6_CR82","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"},{"key":"6_CR83","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 Automat. Electron. Syst. 27(6), 1\u201330 (2022)","DOI":"10.1145\/3514355"},{"key":"6_CR84","doi-asserted-by":"crossref","unstructured":"Janzing, D., Wocjan, P., Beth, T.: \u201cNon-identity-check\u201d is QMA-complete. Int. J. Quant. Inf. 3(03), 463\u2013473 (2005)","DOI":"10.1142\/S0219749905001067"},{"key":"6_CR85","unstructured":"Jeandel, E., Perdrix, S., Veshchezerova, M.: Addition and differentiation of ZX-diagrams. In: Felty, A.P. (ed.) 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 228, pp. 13:1\u201313:19. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2022). https:\/\/drops-dev.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.FSCD.2022.13"},{"key":"6_CR86","unstructured":"Jim\u00e9nez-Pastor, A., Larsen, K.G., Tribastone, M., Tschaikowski, M.: Efficient simulation of quantum circuits by model order reduction. arXiv preprint arXiv:2308.09510 (2023)"},{"key":"6_CR87","unstructured":"de\u00a0Jong, J., Hahn, F., Tcholtchev, N., Hauswirth, M., Pappa, A.: Extracting maximal entanglement from linear cluster states. arXiv preprint arXiv:2211.16758 (2022)"},{"key":"6_CR88","doi-asserted-by":"publisher","unstructured":"Jozsa, R., van\u00a0den Nest, M.: Classical simulation complexity of extended clifford circuits. Quant. Inf. Comput. 14(7\u20138), 633\u2013648 (2014). https:\/\/doi.org\/10.26421\/QIC14.7-8-7","DOI":"10.26421\/QIC14.7-8-7"},{"key":"6_CR89","doi-asserted-by":"crossref","unstructured":"Kim, Y., et al.: Evidence for the utility of quantum computing before fault tolerance. Nature 618(7965), 500\u2013505 (2023)","DOI":"10.1038\/s41586-023-06096-3"},{"key":"6_CR90","doi-asserted-by":"crossref","unstructured":"Kissinger, A., van\u00a0de Wetering, J.: PyZX: large scale automated diagrammatic reasoning. In: QPL (2019). https:\/\/api.semanticscholar.org\/CorpusID:104292461","DOI":"10.4204\/EPTCS.318.14"},{"key":"6_CR91","doi-asserted-by":"publisher","unstructured":"Kissinger, A., van de Wetering, J.: Reducing the number of non-Clifford gates in quantum circuits. Phys. Rev. A 102(2) (2020). https:\/\/doi.org\/10.1103\/PhysRevA.102.022406","DOI":"10.1103\/PhysRevA.102.022406"},{"key":"6_CR92","doi-asserted-by":"publisher","unstructured":"Kissinger, A., van de Wetering, J.: Simulating quantum circuits with ZX-calculus reduced stabiliser decompositions. Quant. Sci. Technol. 7(4), 044001 (2022). https:\/\/doi.org\/10.1088\/2058-9565\/ac5d20","DOI":"10.1088\/2058-9565\/ac5d20"},{"key":"6_CR93","unstructured":"Kissinger, A., van\u00a0de Wetering, J., Vilmart, R.: Classical simulation of quantum circuits with partial and graphical stabiliser decompositions. In: Le\u00a0Gall, F., Morimae, T. (eds.) 17th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 232, pp. 5:1\u20135:13. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2022). https:\/\/drops-dev.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.TQC.2022.5"},{"key":"6_CR94","doi-asserted-by":"crossref","unstructured":"Kitaev, A.Y., Shen, A., Vyalyi, M.N.: Classical and Quantum Computation. American Mathematical Soc. (2002)","DOI":"10.1090\/gsm\/047"},{"key":"6_CR95","doi-asserted-by":"crossref","unstructured":"Koch, M., Yeung, R., Wang, Q.: Speedy contraction of ZX diagrams with triangles via stabiliser decompositions. arXiv preprint arXiv:2307.01803 (2023)","DOI":"10.1088\/1402-4896\/ad6fd8"},{"key":"6_CR96","unstructured":"Kornerup, N., Sadun, J., Soloveichik, D.: The spooky pebble game. arXiv preprint arXiv:2110.08973 (2021)"},{"key":"6_CR97","doi-asserted-by":"crossref","unstructured":"Lai, Y.T., Pedram, M., Vrudhula, S.B.: EVBDD-based algorithms for integer linear programming, spectral transformation, and function decomposition. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 13(8), 959\u2013975 (1994)","DOI":"10.1109\/43.298033"},{"key":"6_CR98","unstructured":"Landahl, A.J., Anderson, J.T., Rice, P.R.: Fault-tolerant quantum computing with color codes. arXiv preprint arXiv:1108.5738 (2011)"},{"key":"6_CR99","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: International Conference on Logic for Programming Artificial Intelligence and Reasoning, pp. 348\u2013370. Springer, Heidelberg (2010)","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"6_CR100","doi-asserted-by":"crossref","unstructured":"Lewis, M., Soudjani, S., Zuliani, P.: Formal verification of quantum programs: theory, tools, and challenges. ACM Trans. Quant. Comput. 5(1), 1\u201335 (2023)","DOI":"10.1145\/3624483"},{"key":"6_CR101","unstructured":"Lin, R.: A graphical calculus for quantum computing with multiple qudits using generalized Clifford algebras (2023)"},{"key":"6_CR102","unstructured":"Lin, S.W., Chen, S.H., Wang, T.F., Chen, Y.R.: A quantum SMT solver for bit-vector theory. arXiv preprint arXiv:2303.09353 (2023)"},{"key":"6_CR103","doi-asserted-by":"publisher","first-page":"436","DOI":"10.22331\/q-2021-04-20-436","volume":"5","author":"N Linden","year":"2021","unstructured":"Linden, N., de Wolf, R.: Lightweight detection of a small number of large errors in a quantum circuit. Quantum 5, 436 (2021)","journal-title":"Quantum"},{"key":"6_CR104","doi-asserted-by":"publisher","unstructured":"Lloyd, S.: Universal quantum simulators. Science 273(5278), 1073\u20131078 (1996). https:\/\/doi.org\/10.1126\/science.273.5278.1073","DOI":"10.1126\/science.273.5278.1073"},{"key":"6_CR105","doi-asserted-by":"crossref","unstructured":"Maslov, D., Falconer, S.M., Mosca, M.: Quantum circuit placement. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 27(4), 752\u2013763 (2008)","DOI":"10.1109\/TCAD.2008.917562"},{"key":"6_CR106","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic model checking: an approach to the state explosion problem. Ph.D. thesis, Carnegie Mellon University (1992)","DOI":"10.1007\/978-1-4615-3190-6_3"},{"key":"6_CR107","doi-asserted-by":"crossref","unstructured":"Mei, J., Bonsangue, M., Laarman, A.: Simulating quantum circuits by model counting. arXiv preprint arXiv:2403.07197 (2024)","DOI":"10.1007\/978-3-031-65633-0_25"},{"key":"6_CR108","doi-asserted-by":"crossref","unstructured":"Mei, J., Coopmans, T., Bonsangue, M., Laarman, A.: Equivalence checking of quantum circuits by model counting. arXiv preprint (to appear) (2024)","DOI":"10.1007\/978-3-031-63501-4_21"},{"issue":"4","key":"6_CR109","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.83.042335","volume":"83","author":"NC Menicucci","year":"2011","unstructured":"Menicucci, N.C., Flammia, S.T., van Loock, P.: Graphical calculus for Gaussian pure states. Phys. Rev. A 83(4), 042335 (2011)","journal-title":"Phys. Rev. A"},{"key":"6_CR110","doi-asserted-by":"publisher","unstructured":"Meuli, G., Soeken, M., De Micheli, G.: SAT-based CNOT, T quantum circuit synthesis. In: Kari, J., Ulidowski, I. (eds.) Reversible Computation, pp. 175\u2013188. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99498-7_12","DOI":"10.1007\/978-3-319-99498-7_12"},{"key":"6_CR111","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), p. 30 (2006)","DOI":"10.1109\/ISMVL.2006.35"},{"key":"6_CR112","doi-asserted-by":"crossref","unstructured":"Molavi, A., Xu, A., Diges, M., Pick, L., Tannu, S., Albarghouthi, A.: Qubit mapping and routing via MaxSAT. In: 2022 55th IEEE\/ACM International Symposium on Microarchitecture (MICRO), pp. 1078\u20131091. IEEE (2022)","DOI":"10.1109\/MICRO56248.2022.00077"},{"key":"6_CR113","doi-asserted-by":"publisher","unstructured":"Montanaro, A.: Quantum algorithms: an overview. NPJ Quant. Inf. 2(1), 15023 (2016). https:\/\/doi.org\/10.1038\/npjqi.2015.23","DOI":"10.1038\/npjqi.2015.23"},{"issue":"1","key":"6_CR114","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4086\/toc.2018.v014a015","volume":"14","author":"A Montanaro","year":"2018","unstructured":"Montanaro, A.: Quantum-walk speedup of backtracking algorithms. Theory Comput. 14(1), 1\u201324 (2018)","journal-title":"Theory Comput."},{"key":"6_CR115","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Kong, S., Avigad, J., Van\u00a0Doorn, F., von Raumer, J.: The Lean theorem prover (system description). In: Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, 1\u20137 August 2015, Proceedings 25, pp. 378\u2013388. Springer, Heidelberg (2015)","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"6_CR116","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1016\/j.micpro.2019.02.005","volume":"66","author":"P Murali","year":"2019","unstructured":"Murali, P., Javadi-Abhari, A., Chong, F.T., Martonosi, M.: Formal constraint-based compilation for noisy intermediate-scale quantum systems. Microprocess. Microsyst. 66, 102\u2013112 (2019)","journal-title":"Microprocess. Microsyst."},{"key":"6_CR117","doi-asserted-by":"crossref","unstructured":"Nagarajan, H., Lockwood, O., Coffrin, C.: QuantumCircuitOpt: an open-source framework for provably optimal quantum circuit design. In: 2021 IEEE\/ACM Second International Workshop on Quantum Computing Software (QCS), pp. 55\u201363. IEEE (2021)","DOI":"10.1109\/QCS54837.2021.00010"},{"key":"6_CR118","unstructured":"Nakamura, K., Denzumi, S., Nishino, M.: Variable shift SDD: a more succinct sentential decision diagram. In: Faro, S., Cantone, D. (eds.) 18th International Symposium on Experimental Algorithms (SEA 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol. 160, pp. 22:1\u201322:13. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2020). https:\/\/drops-dev.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.SEA.2020.22"},{"key":"6_CR119","doi-asserted-by":"crossref","unstructured":"Nannicini, G., Bishop, L.S., G\u00fcnl\u00fck, O., Jurcevic, P.: Optimal qubit assignment and routing via integer programming. ACM Trans. Quant. Comput. 4(1), 1\u201331 (2022)","DOI":"10.1145\/3544563"},{"key":"6_CR120","doi-asserted-by":"crossref","unstructured":"van den Nest, M.: Classical simulation of quantum computation, the Gottesman-Knill theorem, and slightly beyond. Quant. Inf. Comput. 10(3), 258\u2013271 (2010)","DOI":"10.26421\/QIC10.3-4-6"},{"key":"6_CR121","unstructured":"Nielsen, M.A., Chuang, I.L.: Quantum Information and Quantum Computation, vol. 2, no. 8, p. 23. Cambridge University Press, Cambridge (2000)"},{"key":"6_CR122","doi-asserted-by":"crossref","unstructured":"Niemann, P., Wille, R., Drechsler, R.: Equivalence checking in multi-level quantum systems. In: Reversible Computation: 6th International Conference, RC 2014, Kyoto, 10\u201311 July 2014. Proceedings 6, pp. 201\u2013215. Springer, Heidelberg (2014)","DOI":"10.1007\/978-3-319-08494-7_16"},{"key":"6_CR123","doi-asserted-by":"crossref","unstructured":"Niemann, P., Wille, R., Drechsler, R.: Advanced exact synthesis of Clifford+T circuits. Quant. Inf. Process. 19, 1\u201323 (2020)","DOI":"10.1007\/s11128-020-02816-0"},{"key":"6_CR124","doi-asserted-by":"crossref","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)","DOI":"10.1109\/TCAD.2020.2977603"},{"key":"6_CR125","doi-asserted-by":"crossref","unstructured":"Oliveira\u00a0Oliveira, M.D.: On the satisfiability of quantum circuits of small treewidth. Theory Comput. Syst. 61, 656\u2013688 (2017)","DOI":"10.1007\/s00224-016-9727-8"},{"key":"6_CR126","doi-asserted-by":"crossref","unstructured":"Or\u00fas, R.: Tensor networks for complex quantum systems. Nat. Rev. Phys. 1(9), 538\u2013550 (2019)","DOI":"10.1038\/s42254-019-0086-7"},{"key":"6_CR127","doi-asserted-by":"crossref","unstructured":"Or\u00fas, R.: A practical introduction to tensor networks: matrix product states and projected entangled pair states. Annals Phys. 349, 117\u2013158 (2014). https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0003491614001596","DOI":"10.1016\/j.aop.2014.06.013"},{"key":"6_CR128","unstructured":"Oztok, U., Darwiche, A.: A top-down compiler for sentential decision diagrams. In: IJCAI (IJCAI 2015), pp. 3141\u20133148. AAAI Press (2015)"},{"issue":"3","key":"6_CR129","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.128.030501","volume":"128","author":"F Pan","year":"2022","unstructured":"Pan, F., Zhang, P.: Simulation of quantum circuits using the big-batch tensor network method. Phys. Rev. Lett. 128(3), 030501 (2022)","journal-title":"Phys. Rev. Lett."},{"key":"6_CR130","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle","year":"1994","unstructured":"Paulson, L.C. (ed.): Isabelle. LNCS, vol. 828. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/BFb0030541"},{"issue":"3","key":"6_CR131","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. Select. Topics Circuits Syst. 12(3), 662\u2013675 (2022)","journal-title":"IEEE J. Emerg. Select. Topics Circuits Syst."},{"issue":"3","key":"6_CR132","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. Select. Topics Circuits Syst. 12(3), 662\u2013675 (2022)","journal-title":"IEEE J. Emerg. Select. Topics Circuits Syst."},{"key":"6_CR133","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":"6_CR134","unstructured":"Penrose, R.: Applications of negative dimensional tensors. In: Combinatorial Mathematics and its Applications. Academic Press (1971)"},{"key":"6_CR135","doi-asserted-by":"publisher","unstructured":"Perez-Garcia, D., Verstraete, F., Wolf, M., Cirac, J.: Matrix product state representations. Quant. Inf. Comput. 7(5), 401\u2013430 (2007). https:\/\/doi.org\/10.5555\/2011832.2011833","DOI":"10.5555\/2011832.2011833"},{"key":"6_CR136","doi-asserted-by":"publisher","unstructured":"Po\u00f3r, B., Wang, Q., Shaikh, R.A., Yeh, L., Yeung, R., Coecke, B.: Completeness for arbitrary finite dimensions of zxw-calculus, a unifying calculus. In: 2023 38th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). IEEE (2023). https:\/\/doi.org\/10.1109\/LICS56636.2023.10175672","DOI":"10.1109\/LICS56636.2023.10175672"},{"key":"6_CR137","unstructured":"Preskill, J.: Quantum computing and the entanglement frontier. Bull. Am. Phys. Soc. 58 (2013)"},{"key":"6_CR138","doi-asserted-by":"publisher","unstructured":"Preskill, J.: Quantum computing in the NISQ era and beyond. Quantum 2, 79 (2018). https:\/\/doi.org\/10.22331\/q-2018-08-06-79","DOI":"10.22331\/q-2018-08-06-79"},{"key":"6_CR139","doi-asserted-by":"crossref","unstructured":"Quist, A.J., Laarman, A.: Optimizing quantum space using spooky pebble games. In: International Conference on Reversible Computation, pp. 134\u2013149. Springer, Heidelberg (2023)","DOI":"10.1007\/978-3-031-38100-3_10"},{"key":"6_CR140","doi-asserted-by":"crossref","unstructured":"Quist, A.J., Laarman, A.: Trade-offs between classical and quantum space using spooky pebbling. arXiv preprint arXiv:2401.10579 (2024)","DOI":"10.1007\/978-3-031-38100-3_10"},{"key":"6_CR141","doi-asserted-by":"publisher","unstructured":"Raussendorf, R., Briegel, H.J.: A one-way quantum computer. Phys. Rev. Lett. 86, 5188\u20135191 (2001). https:\/\/doi.org\/10.1103\/PhysRevLett.86.5188","DOI":"10.1103\/PhysRevLett.86.5188"},{"key":"6_CR142","doi-asserted-by":"publisher","first-page":"959","DOI":"10.22331\/q-2023-03-23-959","volume":"7","author":"M Rennela","year":"2023","unstructured":"Rennela, M., Brand, S., Laarman, A., Dunjko, V.: Hybrid divide-and-conquer approach for tree search algorithms. Quantum 7, 959 (2023)","journal-title":"Quantum"},{"key":"6_CR143","doi-asserted-by":"crossref","unstructured":"Rieser, H.M., K\u00f6ster, F., Raulf, A.P.: Tensor networks for quantum machine learning. Proc. Roy. Soc. A: Math. Phys. Eng. Sci. 479(2275), 20230218 (2023)","DOI":"10.1098\/rspa.2023.0218"},{"key":"6_CR144","doi-asserted-by":"crossref","unstructured":"Sander, A., Burgholzer, L., Wille, R.: Towards Hamiltonian simulation with decision diagrams. In: 2023 IEEE International Conference on Quantum Computing and Engineering (QCE), vol.\u00a01, pp. 283\u2013294. IEEE (2023)","DOI":"10.1109\/QCE57702.2023.00039"},{"key":"6_CR145","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). https:\/\/api.semanticscholar.org\/CorpusID:52027"},{"key":"6_CR146","doi-asserted-by":"crossref","unstructured":"Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press (2011)","DOI":"10.1017\/CBO9780511777110"},{"key":"6_CR147","doi-asserted-by":"publisher","unstructured":"Sanner, S., McAllester, D.: Affine algebraic decision diagrams (AADDs) and their application to structured probabilistic inference. In: IJCAI, vol. 2005, pp. 1384\u20131390 (2005). https:\/\/doi.org\/10.5555\/1642293.1642513","DOI":"10.5555\/1642293.1642513"},{"key":"6_CR148","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, pp. 190\u2013195 (2023)","DOI":"10.1145\/3566097.3567929"},{"key":"6_CR149","doi-asserted-by":"publisher","first-page":"964","DOI":"10.22331\/q-2023-03-30-964","volume":"7","author":"P Seitz","year":"2023","unstructured":"Seitz, P., Medina, I., Cruz, E., Huang, Q., Mendl, C.B.: Simulating quantum circuits using tree tensor networks. Quantum 7, 964 (2023)","journal-title":"Quantum"},{"key":"6_CR150","doi-asserted-by":"publisher","unstructured":"Selinger, P.: A survey of graphical languages for monoidal categories. In: Coecke, B. (ed.) New Structures for Physics, pp. 289\u2013355. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-12821-9_4","DOI":"10.1007\/978-3-642-12821-9_4"},{"key":"6_CR151","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":"6_CR152","doi-asserted-by":"crossref","unstructured":"Shannon, C.E.: The synthesis of two-terminal switching circuits. Bell Syst. Tech. J. 28(1), 59\u201398 (1949)","DOI":"10.1002\/j.1538-7305.1949.tb03624.x"},{"issue":"1","key":"6_CR153","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevApplied.18.014072","volume":"18","author":"N Shutty","year":"2022","unstructured":"Shutty, N., Chamberland, C.: Decoding merged color-surface codes and finding fault-tolerant Clifford circuits using solvers for satisfiability modulo theories. Phys. Rev. Appl. 18(1), 014072 (2022)","journal-title":"Phys. Rev. Appl."},{"key":"6_CR154","unstructured":"Silva, J.M., Sakallah, K.A.: GRASP-a new search algorithm for satisfiability. In: Proceedings of International Conference on Computer Aided Design, pp. 220\u2013227. IEEE (1996)"},{"key":"6_CR155","doi-asserted-by":"crossref","unstructured":"Sistla, M., Chaudhuri, S., Reps, T.: Symbolic quantum simulation with Quasimodo. In: International Conference on Computer Aided Verification, pp. 213\u2013225. Springer, Heidelberg (2023)","DOI":"10.1007\/978-3-031-37709-9_11"},{"key":"6_CR156","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\/3689760"},{"key":"6_CR157","doi-asserted-by":"crossref","unstructured":"Sistla, M.A., Chaudhuri, S., Reps, T.: CFLOBDDs: context-free-language ordered binary decision diagrams. ACM Trans. Program. Lang. Syst. (2023)","DOI":"10.1145\/3651157"},{"key":"6_CR158","doi-asserted-by":"publisher","unstructured":"Staudacher, K., Guggemos, T., Grundner-Culemann, S., Gehrke, W.: Reducing 2-qubit gate count for ZX-calculus based quantum circuit optimization. Electron. Proc. Theor. Comput. Sci. 394, 29\u201345 (2023). https:\/\/doi.org\/10.4204\/EPTCS.394.3","DOI":"10.4204\/EPTCS.394.3"},{"key":"6_CR159","unstructured":"Tafertshofer, P., Pedram, M.: Factored EVBDDs and their application to matrix representation and manipulation. Tech. rep., CENG Technical Report 94-27, Department of EE-Systems, University of Southern California (1994)"},{"key":"6_CR160","doi-asserted-by":"crossref","unstructured":"Tafertshofer, P., Pedram, M.: Factored edge-valued binary decision diagrams. Formal Methods Syst. Des. 10(2), 243\u2013270 (1997)","DOI":"10.1023\/A:1008691605584"},{"key":"6_CR161","doi-asserted-by":"crossref","unstructured":"Tan, B., Cong, J.: Optimal layout synthesis for quantum computing. In: Proceedings of the 39th International Conference on Computer-Aided Design, pp. 1\u20139 (2020)","DOI":"10.1145\/3400302.3415620"},{"key":"6_CR162","doi-asserted-by":"crossref","unstructured":"Tanaka, Y.: Exact non-identity check is NQP-complete. Int. J. Quant. Inf. 8(05), 807\u2013819 (2010)","DOI":"10.1142\/S0219749910006599"},{"key":"6_CR163","doi-asserted-by":"crossref","unstructured":"Tang, E.: A quantum-inspired classical algorithm for recommendation systems. In: Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing, pp. 217\u2013228 (2019)","DOI":"10.1145\/3313276.3316310"},{"key":"6_CR164","doi-asserted-by":"publisher","unstructured":"Terhal, B.M.: Quantum error correction for quantum memories. Rev. Mod. Phys. 87, 307\u2013346 (2015). https:\/\/doi.org\/10.1103\/RevModPhys.87.307","DOI":"10.1103\/RevModPhys.87.307"},{"key":"6_CR165","doi-asserted-by":"crossref","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, Cham (2023)","DOI":"10.1007\/978-3-031-45332-8_10"},{"key":"6_CR166","doi-asserted-by":"crossref","unstructured":"Thierry-Mieg, Y., Poitrenaud, D., Hamez, A., Kordon, F.: Hierarchical set decision diagrams and regular models. In: TACAS 2009, ETAPS 2009, pp. 1\u201315. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-00768-2_1"},{"key":"6_CR167","doi-asserted-by":"crossref","unstructured":"Toumi, A., Yeung, R., Felice, G.: Diagrammatic differentiation for quantum machine learning. Electron. Proc. Theor. Comput. Sci. 343, 132\u2013144 (2021)","DOI":"10.4204\/EPTCS.343.7"},{"key":"6_CR168","unstructured":"Venturelli, D., et al.: Quantum circuit compilation: an emerging application for automated reasoning. In: Scheduling and Planning Applications Workshop (2019). https:\/\/openreview.net\/forum?id=S1eEBO3nFE"},{"issue":"5","key":"6_CR169","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1023\/B:QINP.0000022725.70000.4a","volume":"2","author":"GF Viamontes","year":"2003","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)","journal-title":"Quantum Inf. Process."},{"key":"6_CR170","doi-asserted-by":"crossref","unstructured":"Viamontes, G.F., Markov, I.L., Hayes, J.P.: Quantum Circuit Simulation. Springer, Cham (2009)","DOI":"10.1007\/978-90-481-3065-8"},{"key":"6_CR171","doi-asserted-by":"crossref","unstructured":"Viamontes, G., Markov, I., Hayes, J.: High-performance QuIDD-based simulation of quantum circuits. In: Proceedings Design, Automation and Test in Europe Conference and Exhibition, vol.\u00a02, pp. 1354\u20131355 (2004)","DOI":"10.1109\/DATE.2004.1269084"},{"key":"6_CR172","doi-asserted-by":"crossref","unstructured":"Villalonga, B., et al.: A flexible high-performance simulator for verifying and benchmarking quantum circuits implemented on real hardware. NPJ Quant. Inf. 5(1), 86 (2019)","DOI":"10.1038\/s41534-019-0196-1"},{"key":"6_CR173","doi-asserted-by":"crossref","unstructured":"Villoria, A., Basold, H., Laarman, A.: Enriching diagrams with algebraic operations. arXiv preprint arXiv:2310.11288 (2023)","DOI":"10.1007\/978-3-031-57228-9_7"},{"key":"6_CR174","doi-asserted-by":"crossref","unstructured":"Vilmart, R.: A near-optimal axiomatisation of ZX-calculus for pure qubit quantum mechanics. arXiv preprint arXiv:1812.09114 (2018)","DOI":"10.1109\/LICS.2019.8785765"},{"key":"6_CR175","unstructured":"Vilmart, R.: Quantum multiple-valued decision diagrams in graphical calculi. In: Bonchi, F., Puglisi, S.J. (eds.) 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol. 202, pp. 89:1\u201389:15. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2021). https:\/\/drops-dev.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.MFCS.2021.89"},{"key":"6_CR176","doi-asserted-by":"publisher","unstructured":"Vinkhuijzen, L., Coopmans, T., Elkouss, D., Dunjko, V., Laarman, A.: LIMDD: a decision diagram for simulation of quantum computing including stabilizer states. Quantum 7, 1108 (2023). https:\/\/doi.org\/10.22331\/q-2023-09-11-1108","DOI":"10.22331\/q-2023-09-11-1108"},{"key":"6_CR177","unstructured":"Vinkhuijzen, L., Coopmans, T., Laarman, A.: A knowledge compilation map for quantum information. arXiv preprint arXiv:2401.01322 (2024)"},{"key":"6_CR178","doi-asserted-by":"crossref","unstructured":"Vinkhuijzen, L., Grurl, T., Hillmich, S., Brand, S., Wille, R., Laarman, A.: Efficient implementation of LIMDDs for quantum circuit simulation. In: International Symposium on Model Checking of Software (SPIN) (2023)","DOI":"10.1007\/978-3-031-32157-3_1"},{"key":"6_CR179","doi-asserted-by":"crossref","unstructured":"Vrudhula, S.B.K., Pedram, M., Lai, Y.T.: Edge Valued Binary Decision Diagrams, pp. 109\u2013132. Springer, New York (1996)","DOI":"10.1007\/978-1-4613-1385-4_5"},{"issue":"3","key":"6_CR180","doi-asserted-by":"publisher","first-page":"1161","DOI":"10.1007\/s10957-023-02229-w","volume":"197","author":"F Wagner","year":"2023","unstructured":"Wagner, F., B\u00e4rmann, A., Liers, F., Weissenb\u00e4ck, M.: Improving quantum computation by optimized qubit routing. J. Optim. Theory Appl. 197(3), 1161\u20131194 (2023)","journal-title":"J. Optim. Theory Appl."},{"key":"6_CR181","doi-asserted-by":"publisher","unstructured":"Wang, Q.: An algebraic axiomatisation of ZX-calculus. Electron. Proc. Theor. Comput. Sci. 340, 303\u2013332 (2021). https:\/\/doi.org\/10.4204\/EPTCS.340.16","DOI":"10.4204\/EPTCS.340.16"},{"key":"6_CR182","unstructured":"Wang, Q., Yeung, R., Koch, M.: Differentiating and integrating ZX diagrams with applications to quantum machine learning (2022)"},{"issue":"2","key":"6_CR183","doi-asserted-by":"publisher","first-page":"584","DOI":"10.1093\/ietfec\/e91-a.2.584","volume":"91","author":"SA 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":"6_CR184","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":"6_CR185","unstructured":"van\u00a0de Wetering, J.: ZX-calculus for the working quantum computer scientist. arXiv preprint arXiv:2012.13966 (2020)"},{"key":"6_CR186","doi-asserted-by":"crossref","unstructured":"Wille, R., Burgholzer, L., Artner, M.: Visualizing decision diagrams for quantum computing (special session summary). In: 2021 Design, Automation and Test in Europe Conference and Exhibition, pp. 768\u2013773. IEEE (2021)","DOI":"10.23919\/DATE51398.2021.9474236"},{"key":"6_CR187","doi-asserted-by":"publisher","unstructured":"Wille, R., Burgholzer, L., Hillmich, S., Grurl, T., Ploier, A., Peham, T.: The basis of design tools for quantum computing: arrays, decision diagrams, tensor networks, and ZX-calculus. In: Proceedings of the 59th ACM\/IEEE Design Automation Conference (DAC 2022), pp. 1367\u20131370. Association for Computing Machinery, New York (2022). https:\/\/doi.org\/10.1145\/3489517.3530627","DOI":"10.1145\/3489517.3530627"},{"key":"6_CR188","doi-asserted-by":"crossref","unstructured":"Wille, R., Hillmich, S., Burgholzer, L.: Tools for quantum computing based on decision diagrams. ACM Trans. Quant. Comput. 3(3), 1\u201317 (2022)","DOI":"10.1145\/3491246"},{"key":"6_CR189","doi-asserted-by":"crossref","unstructured":"Wille, R., Przigoda, N., Drechsler, R.: A compact and efficient SAT encoding for quantum circuits. In: 2013 Africon, pp. 1\u20136. IEEE (2013)","DOI":"10.1109\/AFRCON.2013.6757630"},{"key":"6_CR190","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":"6_CR191","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)"},{"key":"6_CR192","doi-asserted-by":"publisher","unstructured":"Winderl, D., Huang, Q., Mendl, C.B.: A recursively partitioned approach to architecture-aware ZX polynomial synthesis and optimization. In: 2023 IEEE International Conference on Quantum Computing and Engineering (QCE). IEEE (2023). https:\/\/doi.org\/10.1109\/QCE57702.2023.00098","DOI":"10.1109\/QCE57702.2023.00098"},{"key":"6_CR193","unstructured":"de\u00a0Wolf, R.: Quantum computing: lecture notes. arXiv preprint arXiv:1907.09415 (2019)"},{"key":"6_CR194","doi-asserted-by":"crossref","unstructured":"Wood, C.J., Biamonte, J.D., Cory, D.G.: Tensor networks and graphical calculus for open quantum systems. Quant. Info. Comput. 15(9\u201310), 759\u2013811 (2015)","DOI":"10.26421\/QIC15.9-10-3"},{"key":"6_CR195","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":"6_CR196","doi-asserted-by":"crossref","unstructured":"Ying, M.: Floyd-Hoare logic for quantum programs. ACM Trans. Program. Lang. Syst. (TOPLAS) 33(6), 1\u201349 (2012)","DOI":"10.1145\/2049706.2049708"},{"key":"6_CR197","doi-asserted-by":"crossref","unstructured":"Zulehner, A., Hillmich, S., Wille, R.: How to efficiently handle complex values? implementing decision diagrams for quantum computing. In: 2019 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD), pp. 1\u20137. IEEE (2019)","DOI":"10.1109\/ICCAD45719.2019.8942057"},{"key":"6_CR198","doi-asserted-by":"crossref","unstructured":"Zulehner, A., Wille, R.: Improving synthesis of reversible circuits: exploiting redundancies in paths and nodes of QMDDs. In: Reversible Computation: 9th International Conference, RC 2017, Kolkata, 6\u20137 July 2017, Proceedings 9, pp. 232\u2013247. Springer, Heidelberg (2017)","DOI":"10.1007\/978-3-319-59936-6_18"},{"key":"6_CR199","doi-asserted-by":"crossref","unstructured":"Zulehner, A., Wille, R.: Advanced simulation of quantum computations. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 38(5), 848\u2013859 (2019)","DOI":"10.1109\/TCAD.2018.2834427"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-66149-5_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,12]],"date-time":"2024-10-12T07:05:50Z","timestamp":1728716750000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66149-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,13]]},"ISBN":["9783031661488","9783031661495"],"references-count":199,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66149-5_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,10,13]]},"assertion":[{"value":"13 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SPIN","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Model Checking Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","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":"10 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"spin2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/spin-web.github.io\/SPIN2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}