Efficient Quantum Circuit Synthesis for SAT-Oracle With Limited Ancillary Qubit

Abstract

One of the main concerns in the era of noisy intermediate-scale quantum (NISQ) computing and fault-tolerant quantum computing is the optimization of circuit implementation for quantum oracles, particularly with limited resources. Synthesizing a satisfiability (SAT) oracle, a crucial component in solving SAT problems, presents a significant challenge. The current state-of-the-art implementation of an <inline-formula> <tex-math notation="LaTeX">$m$ </tex-math></inline-formula>-clause SAT-oracle necessitates <inline-formula> <tex-math notation="LaTeX">$2m-1$ </tex-math></inline-formula> ancillary qubits and a linear number of elementary gates. We develop two efficient and ancilla-adjustable synthesis algorithms to reduce the overall quantum resource usage. Our first quantum oracle algorithm achieves quadratic optimization in the number of ancillary qubits with merely eight times increased circuit size. We also show that using only three ancillary qubits with quadratic circuit size expansion is enough. Our second algorithm optimizes the circuit depth of the SAT oracle to <inline-formula> <tex-math notation="LaTeX">$\tilde {O}(\log m)$ </tex-math></inline-formula> using <inline-formula> <tex-math notation="LaTeX">$m$ </tex-math></inline-formula> ancillary qubits. By running our algorithms on classical intractable SAT instances featured in SAT competitions, the experiment results show that our required quantum resources align well with our theoretical analysis. Our algorithms highlight the scalability of SAT-oracle-based algorithms in near-term quantum devices, such as Grover’s algorithm.