Quantum algorithms are notoriously hard to design and require significant human ingenuity and insight. We present a new methodology called Quantum Automated Synthesizer (QUASH) that can automatically synthesize quantum circuits using decision procedures that perform symbolic reasoning for combinatorial search. Our automated synthesis approach constructs finite symbolic abstract models of the quantum gates automatically and discovers a quantum circuit as a composition of quantum gates using these symbolic models. Our key insight is that most current quantum algorithms work on a finite number of classical inputs, and hence, their correctness proof relies only on reasoning about a finite set of quantum states that can be represented using finite symbolic systems. We demonstrate the potential of our approach by automatically synthesizing four quantum circuits and re-discovering the Bernstein-Vazirani quantum algorithm using state-of-the-art decision procedures. Our synthesis approach only requires distinguishing between a finite set of symbolic quantum states; for example, the synthesis of the Bernstein-Vazirani quantum algorithm only requires reasoning about the following qubit states- |0, |1, -i|0, i|1, |+, |-, e 1/2 |1i, e iπ/4 |1 and a remaining symbolic state representing all other possible quantum states. Our approach leverages decision procedures and theorem provers to assist in the discovery of new quantum algorithms and is a step towards the automation of quantum algorithm design.
Given a Boolean formula ϕ(x) in conjunctive normal form (CNF), the density of states counts the number of variable assignments that violate exactly e clauses, for all values of e. Thus, the density of states is a histogram of the number of unsatisfied clauses over all possible assignments. This computation generalizes both maximum-satisfiability (MAX-SAT) and model counting problems and not only provides insight into the entire solution space, but also yields a measure for the hardness of the problem instance. Consequently, in real-world scenarios, this problem is typically infeasible even when using state-of-the-art algorithms. While finding an exact answer to this problem is a computationally intensive task, we propose a novel approach for estimating density of states based on the concentration of measure inequalities. The methodology results in a quadratic unconstrained binary optimization (QUBO), which is particularly amenable to quantum annealing-based solutions. We present the overall approach and compare results from the D-Wave quantum annealer against the best-known classical algorithms such as the Hamze-de Freitas-Selby (HFS) algorithm and satisfiability modulo theory (SMT) solvers.