Symbolic Execution of Hadamard-Toffoli Quantum Circuits

The simulation of quantum programs by classical computers is a critical endeavor for several reasons: it provides proof-of-concept validation of quantum algorithms; it provides opportunities to experiment with new programming abstractions suitable for the quantum domain; and most significantly it is a way to explore the elusive boundary at which a quantum advantage may materialize. Here, we show that traditional techniques of symbolic evaluation and partial evaluation yield surprisingly efficient classical simulations for some instances of textbook quantum algorithms that include the Deutsch, Deutsch-Jozsa, Bernstein-Vazirani, Simon, Grover, and Shor's algorithms. The success of traditional partial evaluation techniques in this domain is due to one simple insight: the quantum bits used in these algorithms can be modeled by a symbolic boolean variable while still keeping track of the correlations due to superposition and entanglement. More precisely, the system of constraints generated over the symbolic variables contains all the necessary quantum correlations and hence the answer to the quantum algorithms. With a few programming tricks explained in the paper, quantum circuits with millions of gates can be symbolically executed in seconds. Paradoxically, other circuits with as few as a dozen gates take exponential time. We reflect on the significance of these results in the conclusion.