Document Open Access Logo

Towards a SAT Encoding for Quantum Circuits: A Journey From Classical Circuits to Clifford Circuits and Beyond

Authors Lucas Berent , Lukas Burgholzer , Robert Wille

PDF
Thumbnail PDF

File

LIPIcs.SAT.2022.18.pdf
  • Filesize: 1 MB
  • 17 pages

Document Identifiers

Author Details

Lucas Berent
  • Technical University of Munich, Germany
Lukas Burgholzer
  • Johannes Kepler University Linz, Austria
Robert Wille
  • Technical University of Munich, Germany
  • Software Competence Center Hagenberg GmbH (SCCH), Austria

Funding

This work received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (grant agreement No. 101001318), was part of the Munich Quantum Valley, which is supported by the Bavarian state government with funds from the Hightech Agenda Bayern Plus, and has been supported by the BMK, BMDW, and the State of Upper Austria in the frame of the COMET program (managed by the FFG).

Cite AsGet BibTex

Lucas Berent, Lukas Burgholzer, and Robert Wille. Towards a SAT Encoding for Quantum Circuits: A Journey From Classical Circuits to Clifford Circuits and Beyond. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.SAT.2022.18

Abstract

Boolean Satisfiability (SAT) techniques are well-established in classical computing where they are used to solve a broad variety of problems, e.g., in the design of classical circuits and systems. Analogous to the classical realm, quantum algorithms are usually modelled as circuits and similar design tasks need to be tackled. Thus, it is natural to pose the question whether these design tasks in the quantum realm can also be approached using SAT techniques. To the best of our knowledge, no SAT formulation for arbitrary quantum circuits exists and it is unknown whether such an approach is feasible at all. In this work, we define a propositional SAT encoding that, in principle, can be applied to arbitrary quantum circuits. However, we show that, due to the inherent complexity of representing quantum states, constructing such an encoding is not feasible in general. Therefore, we establish general criteria for determining the feasibility of the proposed encoding and identify classes of quantum circuits fulfilling these criteria. We explicitly demonstrate how the proposed encoding can be applied to the class of Clifford circuits as a representative. Finally, we empirically demonstrate the applicability and efficiency of the proposed encoding for Clifford circuits. With these results, we lay the foundation for continuing the ongoing success of SAT in classical circuit and systems design for quantum circuits.

Subject Classification

ACM Subject Classification
  • Hardware → Electronic design automation
  • Hardware → Quantum computation
Keywords
  • Satisfiability
  • Quantum Computing
  • Design Automation
  • Clifford Circuits

Metrics

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

Supplementary Materials

References

  1. Scott Aaronson and Daniel Gottesman. Improved simulation of stabilizer circuits. Physical Review A, 70(5):052328, 2004. Google Scholar
  2. Matthew Amy and Vlad Gheorghiu. staqemdashA full-stack quantum processing toolkit. Quantum Sci. Technol., 5(3):034016, 2020. Google Scholar
  3. A. Biere, A. Biere, M. Heule, H. van Maaren, and T. Walsh. Handbook of Satisfiability. IOS Press, 2009. Google Scholar
  4. Armin Biere and Daniel Kröning. SAT-based Model Checking. In Handbook of Model Checking, pages 277-303. Springer, 2018. Google Scholar
  5. Adam D. Bookatz. QMA-complete problems. arXiv, 2013. URL: http://arxiv.org/abs/1212.6312.
  6. A. Botea, A. Kishimoto, and Radu Marinescu. On the complexity of quantum circuit compilation. In Int'l Symp. on Combinatorial Search, 2018. Google Scholar
  7. Daniel Brand. Verification of large synthesized designs. In Int'l Conf. on CAD, 1993. Google Scholar
  8. Sergey Bravyi, Dan Browne, Padraic Calpin, Earl Campbell, David Gosset, and Mark Howard. Simulation of quantum circuits by low-rank stabilizer decompositions. Quantum, 3:181, 2019. Google Scholar
  9. Sergey Bravyi, David Gosset, Robert Koenig, and Marco Tomamichel. Quantum advantage with noisy shallow circuits. Nature Physics, 16(10):1040-1045, 2020. Google Scholar
  10. John Brennan et al. Tensor Network Circuit Simulation at Exascale. arXiv, 2021. URL: http://arxiv.org/abs/2110.09894.
  11. Lukas Burgholzer and Robert Wille. Advanced equivalence checking for quantum circuits. IEEE Trans. on CAD of Integrated Circuits and Systems, 2021. Google Scholar
  12. Lukas Burgholzer, Robert Wille, and Richard Kueng. Characteristics of reversible circuits for error detection. arXiv, 2020. URL: http://arxiv.org/abs/201202037.
  13. A Robert Calderbank and Peter W Shor. Good quantum error-correcting codes exist. Physical Review A, 54(2):1098, 1996. Google Scholar
  14. Lu Chin-Yung, Wang Shiou-An, and Kuo Sy-Yen. An extended XQDD representation for multiple-valued quantum logic. IEEE Trans. Comput., pages 1377-1389, 2011. Google Scholar
  15. Ignacio Cirac, David Perez-Garcia, Norbert Schuch, and Frank Verstraete. Matrix Product States and Projected Entangled Pair States: Concepts, Symmetries, and Theorems. arXiv, 2021. URL: http://arxiv.org/abs/2011.12127.
  16. Arianne Meijer-van de Griend and Ross Duncan. Architecture-aware synthesis of phase polynomials for NISQ devices. arXiv, 2020. URL: http://arxiv.org/abs/2004.06052.
  17. Stephan Eggersglüß, Robert Wille, and Rolf Drechsler. Improved SAT-based ATPG: More constraints, better compaction. In Int'l Conf. on CAD, 2013. Google Scholar
  18. Michael P. Frank. The Future of Computing Depends on Making It Reversible. IEEE Spectrum, 2017. Google Scholar
  19. Anteneh Gebregiorgis and Mehdi Baradaran Tahoori. Test pattern generation for approximate circuits based on Boolean satisfiability. In Design, Automation and Test in Europe, 2019. Google Scholar
  20. Brett Giles and Peter Selinger. Exact synthesis of multiqubit Clifford+T circuits. Phys. Rev. A, 87(3):032332, 2013. Google Scholar
  21. Daniel Gottesman. The Heisenberg representation of quantum computers. arXiv, 1998. URL: http://arxiv.org/abs/quant-ph/9807006.
  22. Lov K. Grover. A fast quantum mechanical algorithm for database search. Proc. of the ACM, pages 212-219, 1996. Google Scholar
  23. Thomas Häner, Damian S. Steiger, Krysta Svore, and Matthias Troyer. A software methodology for compiling quantum programs. Quantum Sci. Technol., 3(2):020501, 2018. Google Scholar
  24. Hsin-Yuan Huang, Richard Kueng, and John Preskill. Information-theoretic bounds on quantum advantage in machine learning. Physical Review Letters, 126(19):190505, 2021. Google Scholar
  25. Dominik Janzing, Pawel Wocjan, and Thomas Beth. "Non-identity check" is QMA-complete. Int. J. Quantum Inform., 03(03):463-473, 2005. Google Scholar
  26. Samuel Jaques and Thomas Häner. Leveraging state sparsity for more efficient quantum simulations. arXiv, 2021. URL: http://arxiv.org/abs/2105.01533.
  27. Daniela Kaufmann, Armin Biere, and Manuel Kauers. Verifying large multipliers by combining SAT and computer algebra. In Int'l Conf. on Formal Methods in CAD, pages 28-36, 2019. Google Scholar
  28. T. Larrabee. Test pattern generation using Boolean satisfiability. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst., 11(1):4-15, 1992. Google Scholar
  29. Gushu Li, Yufei Ding, and Yuan Xie. Tackling the qubit mapping problem for NISQ-era quantum devices. In Int'l Conf. on Architectural Support for Programming Languages and Operating Systems, 2019. Google Scholar
  30. D.M. Miller and M.A. Thornton. QMDD: A decision diagram structure for reversible and quantum circuits. In Int'l Symp. on Multi-Valued Logic, 2006. Google Scholar
  31. Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems, 2008. URL: https://github.com/Z3Prover/z3.
  32. Michael A. Nielsen and Isaac L. Chuang. Quantum Computation and Quantum Information. Cambridge University Press, 2010. Google Scholar
  33. Philipp Niemann et al. QMDDs: Efficient quantum function representation and manipulation. IEEE Trans. on CAD of Integrated Circuits and Systems, 2016. Google Scholar
  34. Philipp Niemann, Robert Wille, and Rolf Drechsler. Efficient synthesis of quantum circuits implementing Clifford group operations. In Asia and South Pacific Design Automation Conf., pages 483-488, 2014. Google Scholar
  35. Diego Riste et al. Demonstration of quantum advantage in machine learning. npj Quantum Information, 3(1):1-5, 2017. Google Scholar
  36. Peter W Shor. Scheme for reducing decoherence in quantum computer memory. Physical review A, 52(4):R2493, 1995. Google Scholar
  37. Peter W. Shor. Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer. SIAM J. Comput., 1997. Google Scholar
  38. Kaitlin N. Smith and Mitchell A. Thornton. A quantum computational compiler and design tool for technology-specific targets. In Int'l Symp. on Computer Architecture, 2019. Google Scholar
  39. Andrew M Steane. Error correcting codes in quantum theory. Physical Review Letters, 77(5):793, 1996. Google Scholar
  40. Bochen Tan and Jason Cong. Optimal layout synthesis for quantum computing. In Int'l Conf. on CAD, 2020. Google Scholar
  41. S.-A. Wang, C.-Y. Lu, I-M. Tsai, and S.-Y. Kuo. An XQDD-based verification method for quantum circuits. In IEICE Trans. Fundamentals, pages 584-594, 2008. Google Scholar
  42. Robert Wille, Lukas Burgholzer, and Alwin Zulehner. Mapping quantum circuits to IBM QX architectures using the minimal number of SWAP and H operations. In Design Automation Conf., 2019. Google Scholar
  43. Robert Wille, Daniel Große, Finn Haedicke, and Rolf Drechsler. SMT-based stimuli generation in the SystemC Verification library. In Forum on Specification and Design Languages, 2009. Google Scholar
  44. Robert Wille, Stefan Hillmich, and Lukas Burgholzer. JKQ: JKU tools for quantum computing. In Int'l Conf. on CAD, 2020. Google Scholar
  45. Robert Wille, Nils Przigoda, and Rolf Drechsler. A compact and efficient SAT encoding for quantum circuits. In Africon, 2013. Google Scholar
  46. Robert Wille, Hongyan Zhang, and Rolf Drechsler. ATPG for reversible circuits using simulation, boolean satisfiability, and pseudo boolean optimization. In IEEE Annual Symp. on VLSI, 2011. Google Scholar
  47. David H. Wolpert and William G. Macready. No free lunch theorems for optimization. IEEE Trans. Evol. Comput., 1(1):67-82, 1997. Google Scholar
  48. S. Yamashita and I. L. Markov. Fast equivalence-checking for quantum circuits. In Int'l Symp. on Nanoscale Architectures, 2010. Google Scholar
  49. Alwin Zulehner, Stefan Hillmich, and Robert Wille. How to efficiently handle complex values? Implementing decision diagrams for quantum computing. In Int'l Conf. on CAD, 2019. Google Scholar
  50. Alwin Zulehner and Robert Wille. Advanced simulation of quantum computations. IEEE Trans. on CAD of Integrated Circuits and Systems, 2019. 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