{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T10:31:31Z","timestamp":1768213891220,"version":"3.49.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032156990","type":"print"},{"value":"9783032157003","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-15700-3_7","type":"book-chapter","created":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T07:22:02Z","timestamp":1768202522000},"page":"125-146","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Finding Photonics Circuits via\u00a0$$\\delta $$-Weakening SMT"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4893-7658","authenticated-orcid":false,"given":"Marco","family":"Lewis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1008-5605","authenticated-orcid":false,"given":"Beno\u00eet","family":"Valiron","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,1,13]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","unstructured":"Arrazola, J.M., Di\u00a0Matteo, O., Quesada, N., Jahangiri, S., Delgado, A., Killoran, N.: Universal quantum circuits for quantum chemistry. Quantum 6, 742 (Jun 2022). https:\/\/doi.org\/10.22331\/q-2022-06-20-742","DOI":"10.22331\/q-2022-06-20-742"},{"key":"7_CR2","doi-asserted-by":"publisher","unstructured":"Baldazzi, A., Pavesi, L.: Universal multiport interferometers for post-selected multi-photon gates. Advanced Quantum Technologies p. 2400418 (2024). https:\/\/doi.org\/10.1002\/qute.202400418","DOI":"10.1002\/qute.202400418"},{"key":"7_CR3","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 415\u2013442. Springer International Publishing, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"7_CR4","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Tech. rep., Department of Computer Science, The University of Iowa (2017). available at www.SMT-LIB.org"},{"key":"7_CR5","doi-asserted-by":"publisher","unstructured":"Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 305\u2013343. Springer International Publishing, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"7_CR6","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. (eds.) 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":"7_CR7","doi-asserted-by":"publisher","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.\u00a0236, pp. 18:1\u201318:17. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2022). https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2022.18","DOI":"10.4230\/LIPIcs.SAT.2022.18"},{"issue":"1","key":"7_CR8","doi-asserted-by":"publisher","DOI":"10.1088\/1361-6404\/ad06be","volume":"45","author":"F Bernardini","year":"2023","unstructured":"Bernardini, F., Chakraborty, A., Ord\u00f3\u00f1ez, C.R.: Quantum computing with trapped ions: a beginner\u2019s guide. Eur. J. Phys. 45(1), 013001 (2023). https:\/\/doi.org\/10.1088\/1361-6404\/ad06be","journal-title":"Eur. J. Phys."},{"key":"7_CR9","doi-asserted-by":"publisher","unstructured":"Clarino, D., Seino, K., Matsuo, A., Yamashita, S.: Utilizing don\u2019t-cares to minimize CNOTs in synthesizing NNA compliant quantum circuits. In: 2024 IEEE International Conference on Quantum Computing and Engineering (QCE), vol.\u00a002, pp. 500\u2013501 (2024). https:\/\/doi.org\/10.1109\/QCE60285.2024.10375","DOI":"10.1109\/QCE60285.2024.10375"},{"issue":"12","key":"7_CR10","doi-asserted-by":"publisher","first-page":"1460","DOI":"10.1364\/OPTICA.3.001460","volume":"3","author":"WR Clements","year":"2016","unstructured":"Clements, W.R., Humphreys, P.C., Metcalf, B.J., Kolthammer, W.S., Walmsley, I.A.: Optimal design for universal multiport interferometers. Optica 3(12), 1460\u20131465 (2016). https:\/\/doi.org\/10.1364\/OPTICA.3.001460","journal-title":"Optica"},{"key":"7_CR11","doi-asserted-by":"publisher","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Proceedings of the theory and practice of software, 14th international conference on tools and algorithms for the construction and analysis of systems, pp. 337\u2013340. TACAS\u201908\/ETAPS\u201908, Springer-Verlag, Berlin, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"7_CR12","unstructured":"D.M.Reich.: Characterisation and identification of unitary dynamics maps in terms of their action on density matrices, unpublished"},{"key":"7_CR13","doi-asserted-by":"publisher","unstructured":"Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification, pp. 737\u2013744. Springer International Publishing, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"7_CR14","doi-asserted-by":"publisher","unstructured":"Gao, S., Avigad, J., Clarke, E.M.: $$\\delta $$-complete decision procedures for satisfiability over the reals. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Automated Reasoning, pp. 286\u2013300. Springer Berlin Heidelberg, Berlin, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_23","DOI":"10.1007\/978-3-642-31365-3_23"},{"key":"7_CR15","doi-asserted-by":"publisher","unstructured":"Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) Automated Deduction \u2013 CADE-24, pp. 208\u2013214. Springer Berlin Heidelberg, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_14","DOI":"10.1007\/978-3-642-38574-2_14"},{"key":"7_CR16","unstructured":"D Goerz, M.: Finding the closest unitary for a given matrix. https:\/\/michaelgoerz.net\/notes\/finding-the-closest-unitary-for-a-given-matrix\/ (2014). Accessed14 Sept D2025"},{"key":"7_CR17","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevB.75.165310","volume":"75","author":"L Hormozi","year":"2007","unstructured":"Hormozi, L., Zikos, G., Bonesteel, N.E., Simon, S.H.: Topological quantum compiling. Phys. Rev. B 75, 165310 (2007). https:\/\/doi.org\/10.1103\/PhysRevB.75.165310","journal-title":"Phys. Rev. B"},{"key":"7_CR18","doi-asserted-by":"publisher","unstructured":"Jakobsen, A.B., Clausen, A.B., van\u00a0de Pol, J., Shaik, I.: Depth-optimal quantum layout synthesis as SAT. In: Berg, J., Nordstr\u00f6m, J. (eds.) 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0341, pp. 16:1\u201316:17. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2025). https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2025.16","DOI":"10.4230\/LIPIcs.SAT.2025.16"},{"issue":"1","key":"7_CR19","doi-asserted-by":"publisher","DOI":"10.1088\/1367-2630\/12\/1\/013003","volume":"12","author":"K Kieling","year":"2010","unstructured":"Kieling, K., O\u2019Brien, J.L., Eisert, J.: On photonic controlled phase gates. New J. Phys. 12(1), 013003 (2010). https:\/\/doi.org\/10.1088\/1367-2630\/12\/1\/013003","journal-title":"New J. Phys."},{"issue":"1","key":"7_CR20","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/S0003-4916(02)00018-0","volume":"303","author":"A Kitaev","year":"2003","unstructured":"Kitaev, A.: Fault-tolerant quantum computation by anyons. Ann. Phys. 303(1), 2\u201330 (2003). https:\/\/doi.org\/10.1016\/S0003-4916(02)00018-0","journal-title":"Ann. Phys."},{"key":"7_CR21","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.66.052306","volume":"66","author":"E Knill","year":"2002","unstructured":"Knill, E.: Quantum gates using linear optics and postselection. Phys. Rev. A 66, 052306 (2002). https:\/\/doi.org\/10.1103\/PhysRevA.66.052306","journal-title":"Phys. Rev. A"},{"issue":"6816","key":"7_CR22","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1038\/35051009","volume":"409","author":"E Knill","year":"2001","unstructured":"Knill, E., Laflamme, R., Milburn, G.J.: A scheme for efficient quantum computation with linear optics. Nature 409(6816), 46\u201352 (2001). https:\/\/doi.org\/10.1038\/35051009","journal-title":"Nature"},{"key":"7_CR23","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1103\/RevModPhys.79.135","volume":"79","author":"P Kok","year":"2007","unstructured":"Kok, P., Munro, W.J., Nemoto, K., Ralph, T.C., Dowling, J.P., Milburn, G.J.: Linear optical quantum computing with photonic qubits. Rev. Mod. Phys. 79, 135\u2013174 (2007). https:\/\/doi.org\/10.1103\/RevModPhys.79.135","journal-title":"Rev. Mod. Phys."},{"key":"7_CR24","doi-asserted-by":"publisher","unstructured":"Lewis, M., Valiron, B.: Finding photonics circuits via $$\\delta $$-weakening SMT. Zenodo, v1.0.1 (Sep 2025). https:\/\/doi.org\/10.5281\/zenodo.17233057","DOI":"10.5281\/zenodo.17233057"},{"key":"7_CR25","doi-asserted-by":"publisher","unstructured":"Li, Y., et al.: Quantum Fredkin and Toffoli gates on a versatile programmable silicon photonic chip. npj Quant. Inform. 8(1), 112 (Sep 2022). https:\/\/doi.org\/10.1038\/s41534-022-00627-y","DOI":"10.1038\/s41534-022-00627-y"},{"key":"7_CR26","doi-asserted-by":"publisher","unstructured":"Lin, W.H., Kimko, J., Tan, B., Bj\u00f8rner, N., Cong, J.: Scalable optimal layout synthesis for nisq quantum processors. In: 2023 60th ACM\/IEEE Design Automation Conference (DAC) pp.\u00a01\u20136 (2023). https:\/\/doi.org\/10.1109\/DAC56929.2023.10247760","DOI":"10.1109\/DAC56929.2023.10247760"},{"issue":"5","key":"7_CR27","doi-asserted-by":"publisher","first-page":"2300009","DOI":"10.1002\/qute.202300009","volume":"6","author":"WQ Liu","year":"2023","unstructured":"Liu, W.Q., Wei, H.R.: Linear optical universal quantum gates with higher success probabilities. Adv. Quant. Technol. 6(5), 2300009 (2023). https:\/\/doi.org\/10.1002\/qute.202300009","journal-title":"Adv. Quant. Technol."},{"key":"7_CR28","volume-title":"Quantum Computation and Quantum Information: 10th Anniversary Edition","author":"MA Nielsen","year":"2011","unstructured":"Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information: 10th Anniversary Edition, 10th edn. Cambridge University Press, USA (2011)","edition":"10"},{"key":"7_CR29","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.65.062324","volume":"65","author":"TC Ralph","year":"2002","unstructured":"Ralph, T.C., Langford, N.K., Bell, T.B., White, A.G.: Linear optical controlled-not gate in the coincidence basis. Phys. Rev. A 65, 062324 (2002). https:\/\/doi.org\/10.1103\/PhysRevA.65.062324","journal-title":"Phys. Rev. A"},{"key":"7_CR30","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1103\/PhysRevLett.73.58","volume":"73","author":"M Reck","year":"1994","unstructured":"Reck, M., Zeilinger, A., Bernstein, H.J., Bertani, P.: Experimental realization of any discrete unitary operator. Phys. Rev. Lett. 73, 58\u201361 (1994). https:\/\/doi.org\/10.1103\/PhysRevLett.73.58","journal-title":"Phys. Rev. Lett."},{"key":"7_CR31","doi-asserted-by":"publisher","unstructured":"Seino, K., Yamashita, S.: An SMT-solver-based synthesis of NNA-compliant quantum circuits consisting of CNOT, H and T gates. In: 2023 28th Asia and South Pacific Design Automation Conference (ASP-DAC). pp. 196\u2013201 (2023). https:\/\/doi.org\/10.1145\/3566097.3567931","DOI":"10.1145\/3566097.3567931"},{"key":"7_CR32","doi-asserted-by":"publisher","unstructured":"Shaik, I., van\u00a0de Pol, J.: Optimal layout synthesis for deep quantum circuits on NISQ Processors with 100+ Qubits. In: Chakraborty, S., Jiang, J.H.R. (eds.) 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0305, pp. 26:1\u201326:18. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2024). https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2024.26","DOI":"10.4230\/LIPIcs.SAT.2024.26"},{"key":"7_CR33","doi-asserted-by":"publisher","unstructured":"Yang, J., Kharkov, Y.A., Shi, Y., Heule, M.J.H., Dutertre, B.: Quantum circuit mapping based on incremental and parallel SAT solving. In: Chakraborty, S., Jiang, J.H.R. (eds.) 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0305, pp. 29:1\u201329:18. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2024). https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2024.29","DOI":"10.4230\/LIPIcs.SAT.2024.29"},{"key":"7_CR34","doi-asserted-by":"publisher","unstructured":"Zak, D., Mei, J., Lagniez, J.M., Laarman, A.: Reducing quantum circuit synthesis to #SAT. In: de\u00a0la Banda, M.G. (ed.) 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0340, pp. 38:1\u201338:21. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2025). https:\/\/doi.org\/10.4230\/LIPIcs.CP.2025.38","DOI":"10.4230\/LIPIcs.CP.2025.38"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-15700-3_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T07:22:05Z","timestamp":1768202525000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-15700-3_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032156990","9783032157003"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-15700-3_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"13 January 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rennes","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":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 January 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 January 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/VMCAI-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}