Document Open Access Logo

Quantum Circuit Mapping Based on Incremental and Parallel SAT Solving

Authors Jiong Yang , Yaroslav A. Kharkov, Yunong Shi , Marijn J. H. Heule , Bruno Dutertre

PDF
Thumbnail PDF

File

LIPIcs.SAT.2024.29.pdf
  • Filesize: 1.08 MB
  • 18 pages

Document Identifiers

Author Details

Jiong Yang
  • National University of Singapore, Singapore
Yaroslav A. Kharkov
  • AWS Quantum Technologies, New York, NY, USA
Yunong Shi
  • AWS Quantum Technologies, New York, NY, USA
Marijn J. H. Heule
  • Carnegie Mellon University, Pittsburgh, PA, USA
  • Amazon Web Services, Seattle, WA, USA
Bruno Dutertre
  • Amazon Web Services, Santa Clara, CA, USA

Funding

  • Heule, Marijn J. H.: Supported by the NSF under grant CCF-2229099.

Acknowledgements

Part of the research was conducted during Jiong Yang’s internship at Amazon Web Services. We thank Eric Kessler and Soonho Kong for the insightful discussions on this work. We are grateful to the anonymous reviewers for their constructive comments to improve this paper.

Cite AsGet BibTex

Jiong Yang, Yaroslav A. Kharkov, Yunong Shi, Marijn J. H. Heule, and Bruno Dutertre. Quantum Circuit Mapping Based on Incremental and Parallel SAT Solving. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.SAT.2024.29

Abstract

Quantum Computing (QC) is a new computational paradigm that promises significant speedup over classical computing in various domains. However, near-term QC faces numerous challenges, including limited qubit connectivity and noisy quantum operations. To address the qubit connectivity constraint, circuit mapping is required for executing quantum circuits on quantum computers. This process involves performing initial qubit placement and using the quantum SWAP operations to relocate non-adjacent qubits for nearest-neighbor interaction. Reducing the SWAP count in circuit mapping is essential for improving the success rate of quantum circuit execution as SWAPs are costly and error-prone. In this work, we introduce a novel circuit mapping method by combining incremental and parallel solving for Boolean Satisfiability (SAT). We present an innovative SAT encoding for circuit mapping problems, which significantly improves solver-based mapping methods and provides a smooth trade-off between compilation quality and compilation time. Through comprehensive benchmarking of 78 instances covering 3 quantum algorithms on 2 distinct quantum computer topologies, we demonstrate that our method is 26× faster than state-of-the-art solver-based methods, reducing the compilation time from hours to minutes for important quantum applications. Our method also surpasses the existing heuristics algorithm by 26% in SWAP count.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Compilers
  • Computer systems organization → Quantum computing
  • Computing methodologies → Artificial intelligence
Keywords
  • Quantum computing
  • Quantum compilation
  • SAT solving
  • Incremental solving
  • Parallel solving

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Amira Abbas, Andris Ambainis, Brandon Augustino, Andreas Bärtschi, Harry Buhrman, Carleton Coffrin, Giorgio Cortiana, Vedran Dunjko, Daniel J Egger, Bruce G Elmegreen, et al. Quantum optimization: Potential, challenges, and the path forward. arXiv preprint, 2023. URL: https://arxiv.org/abs/2312.02279.
  2. MD Sajid Anis, Héctor Abraham, R Agarwal AduOffei, Gabriele Agliardi, Merav Aharoni, Ismail Yunus Akhalwaya, Gadi Aleksandrowicz, Thomas Alexander, M Amy, S Anagolum, et al. Qiskit: An open-source framework for quantum computing (2021). SUPPLEMENTARY INFORMATION I. ALGORITHMS II. A RELAXATION BOUND (| E| 2+ 1 9 α| E| 2+ α) Remark, 2021. Google Scholar
  3. Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonell. Cardinality networks and their applications. In Proc. of SAT, 2009. Google Scholar
  4. Gilles Audemard, Jean-Marie Lagniez, Nicolas Szczepanski, and Sébastien Tabary. An adaptive parallel sat solver. In Proc. of CP, 2016. Google Scholar
  5. Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern sat solvers. In Proc. of IJCAI, 2009. Google Scholar
  6. Olivier Bailleux and Yacine Boufkhad. Efficient cnf encoding of boolean cardinality constraints. In Proc. of CP, 2003. Google Scholar
  7. Tomas Balyo, Marijn J.H. Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors. Proceedings of SAT Competition 2022: Solver and Benchmark Descriptions. Department of Computer Science, University of Helsinki, 2022. Google Scholar
  8. Jacob Biamonte, Peter Wittek, Nicola Pancotti, Patrick Rebentrost, Nathan Wiebe, and Seth Lloyd. Quantum machine learning. Nature, 2017. Google Scholar
  9. Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions, 2020. Google Scholar
  10. Adam Bouland, Wim van Dam, Hamed Joorati, Iordanis Kerenidis, and Anupam Prakash. Prospects and challenges of quantum finance. arXiv preprint, 2020. URL: https://arxiv.org/abs/2011.06492.
  11. Fernando G. S. L. Brandão, Amir Kalev, Tongyang Li, Cedric Yen-Yu Lin, Krysta M. Svore, and Xiaodi Wu. Quantum SDP Solvers: Large Speed-ups, Optimality, and Applications to Quantum Learning, 2019. Google Scholar
  12. Markus Büttner and Jussi Rintanen. Satisfiability planning with constraints on the number of actions. In Proc. of ICAPS, 2005. Google Scholar
  13. Yudong Cao, Jonathan Romero, Jonathan P. Olson, Matthias Degroote, Peter D. Johnson, Mária Kieferová, Ian D. Kivlichan, Tim Menke, Borja Peropadre, Nicolas P. D. Sawaya, Sukin Sim, Libor Veis, and Alán Aspuru-Guzik. Quantum chemistry in the age of quantum computing. Chemical Reviews, 2019. Google Scholar
  14. Don Coppersmith. An approximate fourier transform useful in quantum factoring. arXiv preprint quant-ph/0201067, 2002. Google Scholar
  15. Leonardo De Moura and Nikolaj Bjørner. Z3: an efficient smt solver. In Proc. of TACAS, 2008. Google Scholar
  16. Richard P. Feynman. Simulating Physics with Computers. International Journal of Theoretical Physics, 1982. Google Scholar
  17. Craig Gidney and Martin Ekerå. How to factor 2048 bit rsa integers in 8 hours using 20 million noisy qubits. Quantum, 2021. Google Scholar
  18. Andrés Gómez, Álvaro Leitao, Alberto Manzano, Daniele Musso, María R. Nogueiras, Gustavo Ordóñez, and Carlos Vázquez. A Survey on Quantum Computational Finance for Derivatives Pricing and VaR. Archives of Computational Methods in Engineering, 2022. Google Scholar
  19. Youssefa Hamadi, Saidb Jabbour, and Lakhdarb Sais. Manysat: a parallel sat solver issue title: Parallel sat solving. Journal on Satisfiability, Boolean Modeling and Computation, 2009. Google Scholar
  20. Maximilian Heisinger, Mathias Fleury, and Armin Biere. Distributed cube and conquer with paracooba. In Proc. of SAT, 2020. Google Scholar
  21. Dylan Herman, Cody Googin, Xiaoyuan Liu, Alexey Galda, Ilya Safro, Yue Sun, Marco Pistoia, and Yuri Alexeev. A survey of quantum computing for finance. arXiv preprint, 2022. URL: https://arxiv.org/abs/2201.02773.
  22. Marijn J. H. Heule. Chinese remainder encoding for hamiltonian cycles. In Proc. of SAT, 2021. Google Scholar
  23. Marijn J. H. Heule, Oliver Kullmann, Siert Wieringa, and Armin Biere. Cube and conquer: Guiding cdcl sat solvers by lookaheads. In Hardware and Software: Verification and Testing, 2012. Google Scholar
  24. Tomi H. Johnson, Stephen R. Clark, and Dieter Jaksch. What is a quantum simulator? EPJ Quantum Technology, 2014. Google Scholar
  25. Miyuki Koshimura, Tong Zhang, Hiroshi Fujita, and Ryuzo Hasegawa. Qmaxsat: A partial max-sat solver. J. Satisf. Boolean Model. Comput., 2012. Google Scholar
  26. Gushu Li, Yufei Ding, and Yuan Xie. Tackling the qubit mapping problem for nisq-era quantum devices. In Proc. of ASPLOS, 2019. Google Scholar
  27. Jia Hui Liang, Vijay Ganesh, Pascal Poupart, and Krzysztof Czarnecki. Learning rate based branching heuristic for SAT solvers. In Proc. of SAT, 2016. Google Scholar
  28. Wan-Hsuan Lin, Jason Kimko, Bochen Tan, Nikolaj Bjørner, and Jason Cong. Scalable optimal layout synthesis for nisq quantum processors. In Proc. of DAC, 2023. Google Scholar
  29. J.P. Marques Silva and K.A. Sakallah. Conflict analysis in search algorithms for satisfiability. In Proc. of ICTAI, 1996. Google Scholar
  30. Ruben Martins, Saurabh Joshi, Vasco Manquinho, and Inês Lynce. Incremental cardinality constraints for maxsat. In Proc. of CP, 2014. Google Scholar
  31. A. Molavi, A. Xu, M. Diges, L. Pick, S. Tannu, and A. Albarghouthi. Qubit mapping and routing via maxsat. In Proc. of MICRO, 2022. Google Scholar
  32. Michele Mosca, Joao Marcos Vensi Basso, and Sebastian R. Verschoor. On speeding up factoring with quantum SAT solvers. Scientific Reports, 2020. Google Scholar
  33. Michael A. Nielsen and Isaac L. Chuang. Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press, 2010. Google Scholar
  34. Román Orús, Samuel Mugel, and Enrique Lizaso. Quantum computing for finance: Overview and prospects. Reviews in Physics, 2019. Google Scholar
  35. Oxford quantum circuits. https://aws.amazon.com/braket/quantum-computers/oqc/. Accessed: 2024-03-16.
  36. Rigetti computing. https://www.rigetti.com/. Accessed: 2024-02-20.
  37. Dominik Schreiber and Peter Sanders. Scalable sat solving in the cloud. In Proc. of SAT, 2021. Google Scholar
  38. Maria Schuld, Ilya Sinayskiy, and Francesco Petruccione. An introduction to quantum machine learning. Contemporary Physics, 2015. Google Scholar
  39. Peter W. Shor. Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer. SIAM Journal on Computing, 1997. Google Scholar
  40. P.W. Shor. Algorithms for quantum computation: Discrete logarithms and factoring. In Proc. of FOCS, 1994. Google Scholar
  41. Seyon Sivarajah, Silas Dilkes, Alexander Cowtan, Will Simmons, Alec Edgington, and Ross Duncan. t|ket⟩: a retargetable compiler for nisq devices. Quantum Science and Technology, 2020. Google Scholar
  42. Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending SAT solvers to cryptographic problems. In Proc. of SAT, 2009. Google Scholar
  43. Bochen Tan and Jason Cong. Optimality study of existing quantum computing layout synthesis tools. IEEE Transactions on Computers, 2020. Google Scholar
  44. Bochen Tan and Jason Cong. Optimal qubit mapping with simultaneous gate absorption. In Proc. of ICCAD, 2021. Google Scholar
  45. HANTAO ZHANG, MARIA PAOLA BONACINA, and JIEH HSIANG. Psato: a distributed propositional prover and its application to quasigroup problems. Journal of Symbolic Computation, 1996. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact