A SAT Encoding for Optimal Clifford Circuit Synthesis

Sarah Schneider, Lukas Burgholzer, Robert Wille

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

14 Scopus citations

Abstract

Executing quantum algorithms on a quantum computer requires compilation to representations that conform to all restrictions imposed by the device. Due to devices' limited coherence times and gate fidelities, the compilation process has to be optimized as much as possible. To this end, an algorithm's description first has to be synthesized using the device's gate library. In this paper, we consider the optimal synthesis of Clifford circuits-an important subclass of quantum circuits, with various applications. Such techniques are essential to establish lower bounds for (heuristic) synthesis methods and gauging their performance. Due to the huge search space, existing optimal techniques are limited to a maximum of six qubits. The contribution of this work is twofold: First, we propose an optimal synthesis method for Clifford circuits based on encoding the task as a satisfiability (SAT) problem and solving it using a SAT solver in conjunction with a binary search scheme. The resulting tool is demonstrated to synthesize optimal circuits for up to 26 qubits-more than four times as many as the current state of the art. Second, we experimentally show that the overhead introduced by state-of-the-art heuristics exceeds the lower bound by 27 % on average. The resulting tool is publicly available at https://github.com/cda-tum/qmap.

Original languageEnglish
Title of host publicationASP-DAC 2023 - 28th Asia and South Pacific Design Automation Conference, Proceedings
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages190-195
Number of pages6
ISBN (Electronic)9781450397834
DOIs
StatePublished - 16 Jan 2023
Event28th Asia and South Pacific Design Automation Conference, ASP-DAC 2023 - Tokyo, Japan
Duration: 16 Jan 202319 Jan 2023

Publication series

NameProceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC

Conference

Conference28th Asia and South Pacific Design Automation Conference, ASP-DAC 2023
Country/TerritoryJapan
CityTokyo
Period16/01/2319/01/23

Fingerprint

Dive into the research topics of 'A SAT Encoding for Optimal Clifford Circuit Synthesis'. Together they form a unique fingerprint.

Cite this