Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Quantum Reports

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

Chandan Bandyopadhyay, Saibal Majumder, Haresh Kumar Sharma

Published Oct 26, 2026• 0 citations
Publisher

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.

DOI
10.3390/quantum8040111

Related papers

SAT-based Exact Synthesis of Ternary Reversible Circuits using a Functionally Complete Gate Library

Abhoy Kole, Kamalika Datta, Indranil Sengupta +1 more

The problem of synthesis and optimization of reversible and quantum circuits have drawn the attention of researchers for the last two decades due to increasing interest in quantum computing. Although lot of works have been done on the synthesis of binary reversible circuits, very less works have been reported on the synthesis of ternary reversible circuits. Ternary circuits have lower cost of implementation as compared to their binary counterparts. However, the synthesis approaches that exist for ternary reversible circuits either use too many circuit lines (qutrits) or too many gates. Only one prior work has discussed the problem of generating cost-optimal ternary reversible circuits, but for a very restrictive gate library, which limits the approach to a specific subset of ternary reversible functions and often the solution becomes sub-optimal due to the imposed restrictions. The present paper overcomes that restriction, and uses multiple control ternary Toffoli gates with all possible ternary target operations as the gate library. This gate library is functionally complete and can be used to synthesize any arbitrary function. The proposed SAT-based synthesis approach provides low cost solutions in terms of the number of gates for any arbitrary ternary reversible function. Experimental results on various randomly generated permutations as well as standard ternary benchmarks establish this claim. The results can be used as template for other synthesis approaches by observing how far they deviate from the optimal solutions.

Euromicro Conference on Digital System Design (DSD)•Aug 1, 2022•1 citation

Performance Gains in Quantum SAT Solvers Using ESOP Encoding

Majd Assaad, Abhoy Kole, Rolf Drechsler

The Boolean Satisfiability (SAT) problem is a canonical NP-complete problem and a natural candidate for quantum acceleration via search-based algorithms. In Grover-based quantum SAT solvers, the dominant computational cost stems from the construction of a reversible oracle that evaluates the Boolean formula, rendering the choice of SAT encoding crucial for overall quantum resource efficiency. Although SAT instances are conventionally expressed in Conjunctive Normal Form (CNF), such encodings typically translate into quantum circuits with significant qubit overhead and high non-Clifford gate complexity. In this work, we investigate an Exclusive-Sum-of-Products (ESOP)-based CNF (e-CNF) representation tailored for quantum SAT solving and analyze its impact on oracle construction. We derive tighter upper bounds on qubit requirements and Clifford+$T$ gate counts for Grover-based SAT solvers when e-CNF encodings are employed in place of standard CNF. In addition, we propose a scalable transformation from Boolean formulas to e-CNF and present a systematic procedure for interpreting e-CNF representations as reversible quantum circuits suitable for oracle implementation. Experimental evaluation on representative SAT benchmarks demonstrates that the proposed e-CNF-based approach yields substantial and consistent reductions in quantum resources, including qubit count, T-gate complexity, and circuit depth, when compared to CNF-based oracle constructions. These results establish e-CNF as an effective quantum-aware SAT encoding that significantly improves the practicality of oracle-based quantum SAT solving.

quant-pharXiv:2605.16202•May 18, 2026•0 citations

An Algorithm for Synthesis of Reversible Logic Circuits

P. Gupta, Abhinav Agrawal, Niraj Kumar Jha

Reversible logic finds many applications, especially in the area of quantum computing. A completely specified n-input, n-output Boolean function is called reversible if it maps each input assignment to a unique output assignment and vice versa. Logic synthesis for reversible functions differs substantially from traditional logic synthesis and is currently an active area of research. The authors present an algorithm and tool for the synthesis of reversible functions. The algorithm uses the positive-polarity Reed-Muller expansion of a reversible function to synthesize the function as a network of Toffoli gates. At each stage, candidate factors, which represent subexpressions common between the Reed-Muller expansions of multiple outputs, are explored in the order of their attractiveness. The algorithm utilizes a priority-based search tree, and heuristics are used to rapidly prune the search space. The synthesis algorithm currently targets the generalized n-bit Toffoli gate library. However, other algorithms exist that can convert an n-bit Toffoli gate into a cascade of smaller Toffoli gates. Experimental results indicate that the authors' algorithm quickly synthesizes circuits when tested on the set of all reversible functions of three variables. Furthermore, it is able to quickly synthesize all four-variable and most five-variable reversible functions that were in the test suite. The authors also present results for some benchmark functions widely discussed in literature and some new benchmarks that the authors have developed. The algorithm is shown to synthesize many, but not all, randomly generated reversible functions of as many as 16 variables with a maximum gate count of 25

IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems•Oct 30, 2006•379 citations

Factorized Boolean representations for efficient quantum synthesis

Mehul Shah, Robert Fiszer, Marek Perkowski

Quantum algorithms promise advantages beyond classical reach, but running them on error-corrected hardware requires translating Boolean specifications into reversible circuits, and the resources that translation demands determine what is executable. Established methods minimize a Boolean expression and map it to a circuit, assuming the minimized form is best. Here we show that minimized expressions retain algebraic structure minimization cannot reach, arising from containment and complementary-polarity relationships among their terms, and that extracting it yields circuits cheaper to execute despite having more operations. The decisive quantity is not a circuit's operation count but the control count of its widest operation, a superlinear cost; extracting shared factors trades a few wide operations for many narrow ones and reduces qubit count. Across benchmarks and oracles from quantum search and factoring algorithms, at the representation level the transformation never increases either cost measure, a guarantee from its construction. Translation to an executable circuit returns part of that advantage, since auxiliary lines must be uncomputed, yet the factorized circuit still left a leading circuit-level optimizer reaching lower final counts, and faster, than unaided. The representation of a computation is therefore itself a resource, optimizable before compilation and distinct from both logic minimization and circuit-level optimization.

quant-pharXiv:2608.27430•Aug 28, 2026•0 citations

One Additional Qubit is Enough: Encoded Embeddings for Boolean Components in Quantum Circuits

Alwin Zulehner, Philipp Niemann, Rolf Drechsler +1 more

Research on quantum computing has recently gained significant momentum since first physical devices became available. Many quantum algorithms make use of so-called oracles that implement Boolean functions and are queried with highly superposed input states in order to evaluate the implemented Boolean function for many different input patterns in parallel. To simplify or enable a realization of these oracles in quantum logic in the first place, the Boolean reversible functions to be realized usually need to be broken down into several non-reversible sub-functions. However, since quantum logic is inherently reversible, these sub-functions have to be realized in a reversible fashion by adding further qubits in order to make the output patterns distinguishable (a process that is also known as embedding). This usually results in a significant increase of the qubits required in total. In this work, we show how this overhead can be significantly reduced by utilizing coding. More precisely, we prove that one additional qubit is always enough to embed any non-reversible function into a reversible one by using a variable-length encoding of the output patterns. Moreover, we characterize those functions that do not require an additional qubit at all. The made observations show that coding often allows one to undercut the usually considered minimum of additional qubits in sub-functions of oracles by far.

arXiv:1906.02352•IEEE International Symposium on Multiple-Valued Logic (ISMVL)•May 1, 2019•5 citations

Exact Synthesis of Elementary Quantum Gate Circuits for Reversible Functions with Don't Cares

Daniel J. Grosse, Robert Wille, Gerhard W. Dueck +1 more

Compact realizations of reversible logic functions are of interest in the design of quantum computers. In this paper we present an exact synthesis algorithm, based on Boolean satisfiability (SAT), that finds the minimal elementary quantum gate realization for a given reversible function. Since these gates work in terms of qubits, a multi-valued encoding is proposed. Don't care conditions appear naturally in many reversible functions. Constant inputs are often required when a function is embedded into a reversible one. The proposed algorithm takes full advantage of don't care conditions and automatically sets the constant inputs to their optimal values. The effectiveness of the algorithm is shown on a set of benchmark functions.

IEEE International Symposium on Multiple-Valued Logic (ISMVL)•May 1, 2008•47 citations
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.
The problem of synthesis and optimization of reversible and quantum circuits have drawn the attention of researchers for the last two decades due to increasing interest in quantum computing. Although lot of works have been done on the synthesis of binary reversible circuits, very less works have been reported on the synthesis of ternary reversible circuits. Ternary circuits have lower cost of implementation as compared to their binary counterparts. However, the synthesis approaches that exist for ternary reversible circuits either use too many circuit lines (qutrits) or too many gates. Only one prior work has discussed the problem of generating cost-optimal ternary reversible circuits, but for a very restrictive gate library, which limits the approach to a specific subset of ternary reversible functions and often the solution becomes sub-optimal due to the imposed restrictions. The present paper overcomes that restriction, and uses multiple control ternary Toffoli gates with all possible ternary target operations as the gate library. This gate library is functionally complete and can be used to synthesize any arbitrary function. The proposed SAT-based synthesis approach provides low cost solutions in terms of the number of gates for any arbitrary ternary reversible function. Experimental results on various randomly generated permutations as well as standard ternary benchmarks establish this claim. The results can be used as template for other synthesis approaches by observing how far they deviate from the optimal solutions.
The Boolean Satisfiability (SAT) problem is a canonical NP-complete problem and a natural candidate for quantum acceleration via search-based algorithms. In Grover-based quantum SAT solvers, the dominant computational cost stems from the construction of a reversible oracle that evaluates the Boolean formula, rendering the choice of SAT encoding crucial for overall quantum resource efficiency. Although SAT instances are conventionally expressed in Conjunctive Normal Form (CNF), such encodings typically translate into quantum circuits with significant qubit overhead and high non-Clifford gate complexity. In this work, we investigate an Exclusive-Sum-of-Products (ESOP)-based CNF (e-CNF) representation tailored for quantum SAT solving and analyze its impact on oracle construction. We derive tighter upper bounds on qubit requirements and Clifford+TTT gate counts for Grover-based SAT solvers when e-CNF encodings are employed in place of standard CNF. In addition, we propose a scalable transformation from Boolean formulas to e-CNF and present a systematic procedure for interpreting e-CNF representations as reversible quantum circuits suitable for oracle implementation. Experimental evaluation on representative SAT benchmarks demonstrates that the proposed e-CNF-based approach yields substantial and consistent reductions in quantum resources, including qubit count, T-gate complexity, and circuit depth, when compared to CNF-based oracle constructions. These results establish e-CNF as an effective quantum-aware SAT encoding that significantly improves the practicality of oracle-based quantum SAT solving.
Reversible logic finds many applications, especially in the area of quantum computing. A completely specified n-input, n-output Boolean function is called reversible if it maps each input assignment to a unique output assignment and vice versa. Logic synthesis for reversible functions differs substantially from traditional logic synthesis and is currently an active area of research. The authors present an algorithm and tool for the synthesis of reversible functions. The algorithm uses the positive-polarity Reed-Muller expansion of a reversible function to synthesize the function as a network of Toffoli gates. At each stage, candidate factors, which represent subexpressions common between the Reed-Muller expansions of multiple outputs, are explored in the order of their attractiveness. The algorithm utilizes a priority-based search tree, and heuristics are used to rapidly prune the search space. The synthesis algorithm currently targets the generalized n-bit Toffoli gate library. However, other algorithms exist that can convert an n-bit Toffoli gate into a cascade of smaller Toffoli gates. Experimental results indicate that the authors' algorithm quickly synthesizes circuits when tested on the set of all reversible functions of three variables. Furthermore, it is able to quickly synthesize all four-variable and most five-variable reversible functions that were in the test suite. The authors also present results for some benchmark functions widely discussed in literature and some new benchmarks that the authors have developed. The algorithm is shown to synthesize many, but not all, randomly generated reversible functions of as many as 16 variables with a maximum gate count of 25
Quantum algorithms promise advantages beyond classical reach, but running them on error-corrected hardware requires translating Boolean specifications into reversible circuits, and the resources that translation demands determine what is executable. Established methods minimize a Boolean expression and map it to a circuit, assuming the minimized form is best. Here we show that minimized expressions retain algebraic structure minimization cannot reach, arising from containment and complementary-polarity relationships among their terms, and that extracting it yields circuits cheaper to execute despite having more operations. The decisive quantity is not a circuit's operation count but the control count of its widest operation, a superlinear cost; extracting shared factors trades a few wide operations for many narrow ones and reduces qubit count. Across benchmarks and oracles from quantum search and factoring algorithms, at the representation level the transformation never increases either cost measure, a guarantee from its construction. Translation to an executable circuit returns part of that advantage, since auxiliary lines must be uncomputed, yet the factorized circuit still left a leading circuit-level optimizer reaching lower final counts, and faster, than unaided. The representation of a computation is therefore itself a resource, optimizable before compilation and distinct from both logic minimization and circuit-level optimization.
Research on quantum computing has recently gained significant momentum since first physical devices became available. Many quantum algorithms make use of so-called oracles that implement Boolean functions and are queried with highly superposed input states in order to evaluate the implemented Boolean function for many different input patterns in parallel. To simplify or enable a realization of these oracles in quantum logic in the first place, the Boolean reversible functions to be realized usually need to be broken down into several non-reversible sub-functions. However, since quantum logic is inherently reversible, these sub-functions have to be realized in a reversible fashion by adding further qubits in order to make the output patterns distinguishable (a process that is also known as embedding). This usually results in a significant increase of the qubits required in total. In this work, we show how this overhead can be significantly reduced by utilizing coding. More precisely, we prove that one additional qubit is always enough to embed any non-reversible function into a reversible one by using a variable-length encoding of the output patterns. Moreover, we characterize those functions that do not require an additional qubit at all. The made observations show that coding often allows one to undercut the usually considered minimum of additional qubits in sub-functions of oracles by far.
Compact realizations of reversible logic functions are of interest in the design of quantum computers. In this paper we present an exact synthesis algorithm, based on Boolean satisfiability (SAT), that finds the minimal elementary quantum gate realization for a given reversible function. Since these gates work in terms of qubits, a multi-valued encoding is proposed. Don't care conditions appear naturally in many reversible functions. Constant inputs are often required when a function is embedded into a reversible one. The proposed algorithm takes full advantage of don't care conditions and automatically sets the constant inputs to their optimal values. The effectiveness of the algorithm is shown on a set of benchmark functions.