SAT-Guided Conversion of Boolean Functions into Reversible Quantum Logic: Minimal Embedding, Exact Synthesis, and Cost-Aware Mapping

Full abstract

Read the full abstract

A classical Boolean specification need not be one-to-one, whereas every reversible quantum network must preserve distinctions between basis states. SAT-Embed-Q handles this mismatch by first constructing a partial reversible embedding from output-preimage multiplicities and then searching for a compatible mixed-polarity Toffoli network. We implemented two bounded satisfiability encodings, one tracking complete intermediate states and the other tracking individual line values, and evaluated both with a deterministic reference DPLL solver. On the four-line example F(a,b,c)=ab¯∨bc, the minimum-depth CNF contains 42,234 clauses in the direct encoding and 34,194 in the bit-level encoding. The smaller clause set did not translate into faster execution: the direct representation required less time in our solver. A separate exhaustive study of the target-preserving oracle class covers every single-output function of two and three inputs. Within that restricted class, allowing negative controls lowers the summed minimum target-gate count by 34.38% and 46.39%, respectively. We also examine two four-input functions from RevLib, for which fixing the input-preserving oracle structure leads to different gate counts from embedding-optimized benchmark circuits. These experiments characterize bounded synthesis and control-polarity choices for small functions; fault-tolerant resource optimization and large-network scalability remain outside their scope.