Search

Boolean matching is an important problem in logic synthesis and verification. Despite being well-studied for conventional Boolean circuits, its treatment for reversible logic circuits remains largely, if not completely, missing. This work provides the first such study. Given two (black-box) reversible logic circuits that are promised to be matchable, we check their equivalences under various input/output negation and permutation conditions subject to the availability/unavailability of their inverse circuits. Notably, among other results, we show that the equivalence up to input negation and permutation is solvable in quantum polynomial time, while its classical complexity is exponential. This result is arguably the first demonstration of quantum exponential speedup in solving design automation problems. Also, as a negative result, we show that the equivalence up to both input and output negations is not solvable in quantum polynomial time unless UNIQUE-SAT is, which is unlikely. This work paves the theoretical foundation of Boolean matching reversible circuits for potential applications, e.g., in quantum circuit synthesis.

This paper addresses the challenge of preparing arbitrary mixed quantum states, an area that has not been extensively studied compared to pure states. Two circuit design methods are presented: one via a mixture of pure states and the other via purification. A novel strategy utilizing the Cholesky decomposition is proposed to improve both computational efficiency during preprocessing and circuit efficiency in the resulting circuits, offering significant advantages, especially when the targeted density matrix is low-ranked or sparse. By leveraging the incomplete Cholesky decomposition with threshold dropping, we also propose an appealing strategy for generating a high-fidelity approximation of the targeted density matrix, enabling substantial efficiency enhancement at the cost of mild fidelity loss. Additionally, as a closely related issue, we prove the "no-superposing theorem": given a certain number of arbitrary unknown pure states as input, it is impossible to devise an operation that produces an output state as the superposition of the input states with predefined coefficients unless all but one of the coefficients vanish., Comment: 25 pages, 8 figures

Equivalence checking of quantum circuits is an essential element in quantum program compilation, in which a quantum program can be synthesized into different quantum circuits that may vary in the number of qubits, initialization requirements, and output states. Verifying the equivalences among the implementation variants requires proper generality. Although different notions of quantum circuit equivalence have been defined, prior methods cannot check observational equivalence between two quantum circuits whose qubits are partially initialized, which is referred to as partial equivalence. In this work, we prove a necessary and sufficient condition for two circuits to be partially equivalent. Based on the condition, we devise algorithms for checking quantum circuits whose partial equivalence cannot be verified by prior approaches. Experiment results confirm the generality and demonstrate the efficiency and effectiveness of our method. Our result may unleash the optimization power of quantum program compilation to take more aggressive steps., Comment: accepted by QCE22

Logic synthesis is a fundamental step in hardware design whose goal is to find structural representations of Boolean functions while minimizing delay and area. If the function is completely-specified, the implementation accurately represents the function. If the function is incompletely-specified, the implementation has to be true only on the care set. While most of the algorithms in logic synthesis rely on SAT and Boolean methods to exactly implement the care set, we investigate learning in logic synthesis, attempting to trade exactness for generalization. This work is directly related to machine learning where the care set is the training set and the implementation is expected to generalize on a validation set. We present learning incompletely-specified functions based on the results of a competition conducted at IWLS 2020. The goal of the competition was to implement 100 functions given by a set of care minterms for training, while testing the implementation using a set of validation minterms sampled from the same function. We make this benchmark suite available and offer a detailed comparative analysis of the different approaches to learning, Comment: In this 23 page manuscript, we explore the connection between machine learning and logic synthesis which was the main goal for International Workshop on logic synthesis. It includes approaches applied by ten teams spanning 6 countries across the world

Quantum computing is greatly advanced in recent years and is expected to transform the computation paradigm in the near future. Quantum circuit simulation plays a key role in the toolchain for the development of quantum hardware and software systems. However, due to the enormous Hilbert space of quantum states, simulating quantum circuits with classical computers is extremely challenging despite notable efforts have been made. In this paper, we enhance quantum circuit simulation in two dimensions: accuracy and scalability. The former is achieved by using an algebraic representation of complex numbers; the latter is achieved by bit-slicing the number representation and replacing matrix-vector multiplication with symbolic Boolean function manipulation. Experimental results demonstrate that our method can be superior to the state-of-the-art for various quantum circuits and can simulate certain benchmark families with up to tens of thousands of qubits., Comment: 9 pages, 2 figures

Stochastic Boolean Satisfiability (SSAT) is a logical formalism to model decision problems with uncertainty, such as Partially Observable Markov Decision Process (POMDP) for verification of probabilistic systems. SSAT, however, is limited by its descriptive power within the PSPACE complexity class. More complex problems, such as the NEXPTIME-complete Decentralized POMDP (Dec-POMDP), cannot be succinctly encoded with SSAT. To provide a logical formalism of such problems, we extend the Dependency Quantified Boolean Formula (DQBF), a representative problem in the NEXPTIME-complete class, to its stochastic variant, named Dependency SSAT (DSSAT), and show that DSSAT is also NEXPTIME-complete. We demonstrate the potential applications of DSSAT to circuit synthesis of probabilistic and approximate design. Furthermore, to study the descriptive power of DSSAT, we establish a polynomial-time reduction from Dec-POMDP to DSSAT. With the theoretical foundations paved in this work, we hope to encourage the development of DSSAT solvers for potential broad applications., Comment: 10 pages, 5 figures. A condensed version of this work is published in the AAAI Conference on Artificial Intelligence (AAAI) 2021

It is often difficult to correctly implement a Boolean controller for a complex system, especially when concurrency is involved. Yet, it may be easy to formally specify a controller. For instance, for a pipelined processor it suffices to state that the visible behavior of the pipelined system should be identical to a non-pipelined reference system (Burch-Dill paradigm). We present a novel procedure to efficiently synthesize multiple Boolean control signals from a specification given as a quantified first-order formula (with a specific quantifier structure). Our approach uses uninterpreted functions to abstract details of the design. We construct an unsatisfiable SMT formula from the given specification. Then, from just one proof of unsatisfiability, we use a variant of Craig interpolation to compute multiple coordinated interpolants that implement the Boolean control signals. Our method avoids iterative learning and back-substitution of the control functions. We applied our approach to synthesize a controller for a simple two-stage pipelined processor, and present first experimental results., Comment: This paper originally appeared in FMCAD 2013, http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD13/index.shtml. This version includes an appendix that is missing in the conference version

Perturbation theory in quantum mechanics studies how quantum systems interact with their environmental perturbations. Harmonic perturbation is a rare special case of time-dependent perturbations in which exact analysis exists. Some important technology advances, such as masers, lasers, nuclear magnetic resonance, etc., originated from it. Here we add quantum computation to this list with a theoretical demonstration. Based on harmonic perturbation, a quantum mechanical algorithm is devised to search the ground state of a given Hamiltonian. The intrinsic complexity of the algorithm is continuous and parametric in both time T and energy E. More precisely, the probability of locating a search target of a Hamiltonian in N-dimensional vector space is shown to be 1/(1+ c N E^{-2} T^{-2}) for some constant c. This result is optimal. As harmonic perturbation provides a different computation mechanism, the algorithm may suggest new directions in realizing quantum computers., Comment: 6 pages, 4 figures, revtex4