Recently, a practical quantum annealing device has been commercialized by D-Wave Systems, sparking research interest in developing applications to solve problems that are intractable for classical computer. This paper provides a tutorial for using quantum annealer to solve Boolean satisfiability problem. We explain the computational model of quantum annealer and discuss the detailed mapping technique inspired by FPGA CAD flow, including stages such as logic optimization, placement and routing.

Recent research has demonstrated promising results in solving constrained satisfaction problem (CSP) using D-Wave quantum annealer. However, the embedding of the CSP suffers drawbacks such as long embedding time in addition to poor quality due to long chains that reduce the ground state probability. To address those issues, we propose an effective embedding technique that reduces the embedding time and minimizes the chain length. We compared to the most recent method published in DAC 2016. Experiments using existing D-Wave 2X quantum annealer show that the proposed embedding technique increases the ground state probability by 29% on average. Furthermore, to demonstrate the efficiency, we embedded large problems onto a predicted C100 D-Wave Chimera architecture. Experimental results show that our approach reduces the run-time by 3.4x on average with reduced longest chain length.

Quantum annealing device has shown a great potential in solving discrete problems that are theoretically and empirically hard. Boolean Satisfiability (SAT) problem, determining if there is an assignment of variables that satisfies a given Boolean function, is the first proven NP-complete problem widely used in various domains. Here, we present a novel mapping of the SAT problem to the quadratic unconstrained binary optimization problem (QUBO), and further develop a tool flow embedding the proposed QUBO to the architecture of the commercialized quantum computer D-Wave. By leveraging electronic design automation techniques including synthesis, placement and routing, this is not only the first work providing the detail flow that embeds the QUBO, but also a technique scalable for real world applications and some hard SAT problems with over 6000 variables in QUBO. Based on our results, we discuss the challenges in solving SAT using the current generation of annealing device, and explore the problem solving capability of future quantum annealing computers.

In this paper, we present HCS - Heterogeneous CRAM Scrubbing - for FPGAs. By utilizing stochastic fault modeling for SEUs in CRAM, we present a quantitative estimate of system MTTF improvement through CRAM scrubbing. HCS then leverages the fact that different SEUs have unequal effects on the circuit system operation, and thus the CRAM bits can be scrubbed at different rates based on the sensitivity of the bits to the circuit system failures. To maximize the improvement on system MTTF for a given circuit system, we present a dynamic programming algorithm which solves the problem efficiently and effectively. Through a detailed case study on system level study by an H.264/AVC decoder implemented on a Xilinx Virtex-5 FPGA, we show an estimation of 60% MTTF improvement by HCS over the existing homogeneous CRAM scrubbing method, while contributing virtually no area, performance and power overhead to the system.