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

IEEE International Conference on Computer Design: VLSI in Computers and Processors (ICCD)

A Quantum Method to Match Vector Boolean Functions using Simon's Solver

M. Vénere, Alessandro Barenghi, Gerardo Pelosi

Published Nov 18, 2024• 3 citations
Publisher

Abstract

The Boolean Matching Problem is a fundamental step in modern Electronic Design Automation toolchains, which allow the efficient design of large classical computers. In particular, the equivalence under negation-permutation-negation of two n-to-n vector Boolean functions requires the exploration of a super-exponential number of possible negations and permutations of input and output variables, and is widely regarded as a daunting challenge. Its classical complexity$(\mathcal{O}(n!2^{2n})$, where$n$is the number of input and output variables) is rarely tolerated by EDA tools, which are typically solving small instances of the Boolean Matching Problem for n-to-1 Boolean functions. In this work, we present a method to exploit the solver for Simon's problem to speedup the matching of n-to-n vector Boolean functions, as we show that, despite its higher complexity, it is friendlier to a quantum solver than matching single-output Boolean functions. Our solution allows saving a factor$2^{n}$in the overall worst-case computational effort, and is amenable to combined approaches such as the so-called Grover-meets-Simon, which have the potential of reducing it below the cost of classical n-to-1 matching. We provide a fully detailed quantum circuit implementing our proposal, and compute its cost, both counting the required amount of qubits and quantum gates. We conducted an experimental evaluation employing the ISCAS benchmark suite, a de-facto standard for classical EDA to derive our sample Boolean functions.

DOI
10.1109/iccd63220.2024.00089

Related papers

A Grover-Meets-Simon Approach to Match Vector Boolean Functions

M. Vénere, Alessandro Barenghi, Gerardo Pelosi

The Boolean Matching Problem via$NP$-Equivalence requires determining whether two Boolean functions are equivalent or not up to a permutation and negation of the input binary variables. Its solution is a fundamental step in the Electronic Design Automation (EDA) tool chains commonly used for digital circuit design. In fact, thelibrary-mappingstep of an EDA workflow requires matching parts of the gate-level design (netlist) with the components available in a technology library, considering them as Boolean functions, while taking into account that permutations and negations of input variables can be efficiently implemented through rewiring and the use of inverters. For$n$-to-$n$vector Boolean functions, where$n$is the number of input and output variables, the search space of possible negations and permutations is super-exponential in size, while the$\mathcal {O}(n!n2^{2n})$time complexity of classical approaches allows solving only small instances of the$NP$-problem, often limited to$n$-to-1 Boolean functions (executing$\mathcal {O}(n!2^{2n})$bit operations). This work presents a quantum algorithm for matching$n$-to-$n$vector Boolean functions by effectively combining the Grover-meets-Simon approach with an original and novel use of the Simon solver without the constraints imposed by its usual premises. We provide a fully detailed quantum circuit implementing our proposal, calculate its cost by evaluating key performance indicators for circuit synthesis and show an exponential speedup over classical solutions. Finally, we validate our approach on the Boolean functions included in the ISCAS benchmark suite, which are of practical interest in EDA.

IEEE Transactions on Quantum Engineering•Jan 1, 2025•0 citations

Boolean Matching Reversible Circuits: Algorithm and Complexity

Tian-Fu Chen, Jie-Hong Roland Jiang

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.

arXiv:2404.12184•ACM/IEEE Design Automation Conference (DAC)•Jun 23, 2024•4 citations

Quantangle-SAT: A Quantum SAT Solver Based on Entanglement and Equivalence Checking

Shang-Wei Lin, Ji-Qing Yan, Yean-Ru Chen +2 more

Satisfiability (SAT) is a central problem in computer science, and advances in SAT-solving algorithms have a far-reaching impact across many fields. Recent works have proposed quantum SAT solvers based on Grover's algorithm, a quantum search technique. However, Grover-based approaches face a key limitation: they typically require prior knowledge of the number of satisfying assignments of the target Boolean formula. This information is unavailable in most practical settings. Quantum counting can be used to estimate this quantity, but it incurs a computational overhead that is several orders of magnitude higher than Grover search. In this paper, we propose a novel quantum SAT solver based on entanglement and equivalence checking. Our method does not assume prior knowledge of the number of solutions and is computationally more efficient than quantum counting. Although the worst case time complexity is inevitably exponential, we prove that the expected time complexity of our approach is only constant time O(1) over random Boolean functions. Experimental results also support our theoretical claim.

quant-pharXiv:2604.18218•Apr 21, 2026•0 citations

Pushing the number of qubits below the “minimum”: Realizing compact boolean components for quantum logic

Alwin Zulehner, Robert Wille

Research on quantum computers has gained attention since they are able to solve certain tasks significantly faster than classical machines (in some cases, exponential speed-ups are possible). Since quantum computations typically contain large Boolean components, design automation techniques are required to realize the respective Boolean functions in quantum logic. They usually introduce a significant amount of additional qubits - a highly limited resource. In this work, we propose an alternative method for the realization of Boolean components for quantum logic. In contrast to the current state-of-the-art, we dedicatedly address the main reasons causing the additionally required qubits (namely the number of the most frequently occurring output pattern as well as the number of primary outputs of the function to be realized) and propose to manipulate the function so that both issues are addressed. The resulting methods allow to push the number of required qubits below what is currently considered the minimum.

Design, Automation, and Test in Europe•Mar 1, 2018•2 citations

Automated Theorem Proving for Quantum Circuit Verification using SAT Solvers

Jincheng Zhang

The verification of quantum circuits is a critical task in quantum computing, ensuring the fidelity and correctness of quantum computations. However, the exponential scaling of the problem with circuit size presents a significant challenge. This paper proposes a novel approach to automated theorem proving for quantum circuit verification by formulating the verification problem as a Boolean satisfiability (SAT) problem. We demonstrate a methodology for translating quantum circuit properties (e.g., output state, gate operations) into equivalent Boolean expressions and subsequently employing existing SAT solvers to determine the satisfiability of these expressions. This approach effectively bridges the gap between quantum circuit theory and SAT solving, offering a potentially scalable solution for verifying complex quantum circuits. The core of our system revolves around a translation module that converts quantum circuit specifications into SAT instances, and a solver interface that interacts with established SAT solvers. We explore the limitations of this approach and discuss future research directions, including hybrid approaches combining SAT solving with quantum simulation techniques. The effectiveness of this method is demonstrated through theoretical analysis and conceptual design, with a focus on the algorithmic efficiency and potential scalability of the proposed framework.

•Sep 5, 2026•0 citations

Solving Boolean Satisfiability Problems With The Quantum Approximate Optimization Algorithm

Sami Boulebnane, Ashley Montanaro

One of the most prominent application areas for quantum computers is solving hard constraint satisfaction and optimization problems. However, detailed analyses of the complexity of standard quantum algorithms have suggested that outperforming classical methods for these problems would require extremely large and powerful quantum computers. The quantum approximate optimization algorithm (QAOA) is designed for near-term quantum computers, yet previous work has shown strong limitations on the ability of QAOA to outperform classical algorithms for optimization problems. Here we instead apply QAOA to hard constraint satisfaction problems, where both classical and quantum algorithms are expected to require exponential time. We analytically characterize the average success probability of QAOA on a constraint satisfaction problem commonly studied using statistical physics methods: random k -SAT at the threshold for satisfiability, as the number of variables n goes to infinity. We complement these theoretical results with numerical experiments on the performance of QAOA for small n , which match the limiting theoretical bounds closely. We then compare QAOA with leading classical solvers. For random 8-SAT, we find that for more than 14 quantum circuit layers, QAOA achieves more efficient scaling than the highest-performance classical solver we tested, WalkSATlm. Our results suggest that near-term quantum algorithms for solving constraint satisfaction problems may outperform their classical counterparts. Published by the American Physical Society 2024

arXiv:2208.06909•PRX Quantum•Sep 10, 2024•57 citations
The Boolean Matching Problem is a fundamental step in modern Electronic Design Automation toolchains, which allow the efficient design of large classical computers. In particular, the equivalence under negation-permutation-negation of two n-to-n vector Boolean functions requires the exploration of a super-exponential number of possible negations and permutations of input and output variables, and is widely regarded as a daunting challenge. Its classical complexity(O(n!22n)(\mathcal{O}(n!2^{2n})(O(n!22n), wherennnis the number of input and output variables) is rarely tolerated by EDA tools, which are typically solving small instances of the Boolean Matching Problem for n-to-1 Boolean functions. In this work, we present a method to exploit the solver for Simon's problem to speedup the matching of n-to-n vector Boolean functions, as we show that, despite its higher complexity, it is friendlier to a quantum solver than matching single-output Boolean functions. Our solution allows saving a factor2n2^{n}2nin the overall worst-case computational effort, and is amenable to combined approaches such as the so-called Grover-meets-Simon, which have the potential of reducing it below the cost of classical n-to-1 matching. We provide a fully detailed quantum circuit implementing our proposal, and compute its cost, both counting the required amount of qubits and quantum gates. We conducted an experimental evaluation employing the ISCAS benchmark suite, a de-facto standard for classical EDA to derive our sample Boolean functions.
The Boolean Matching Problem viaNPNPNP-Equivalence requires determining whether two Boolean functions are equivalent or not up to a permutation and negation of the input binary variables. Its solution is a fundamental step in the Electronic Design Automation (EDA) tool chains commonly used for digital circuit design. In fact, thelibrary-mappingstep of an EDA workflow requires matching parts of the gate-level design (netlist) with the components available in a technology library, considering them as Boolean functions, while taking into account that permutations and negations of input variables can be efficiently implemented through rewiring and the use of inverters. Fornnn-to-nnnvector Boolean functions, wherennnis the number of input and output variables, the search space of possible negations and permutations is super-exponential in size, while theO(n!n22n)\mathcal {O}(n!n2^{2n})O(n!n22n)time complexity of classical approaches allows solving only small instances of theNPNPNP-problem, often limited tonnn-to-1 Boolean functions (executingO(n!22n)\mathcal {O}(n!2^{2n})O(n!22n)bit operations). This work presents a quantum algorithm for matchingnnn-to-nnnvector Boolean functions by effectively combining the Grover-meets-Simon approach with an original and novel use of the Simon solver without the constraints imposed by its usual premises. We provide a fully detailed quantum circuit implementing our proposal, calculate its cost by evaluating key performance indicators for circuit synthesis and show an exponential speedup over classical solutions. Finally, we validate our approach on the Boolean functions included in the ISCAS benchmark suite, which are of practical interest in EDA.
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.
Satisfiability (SAT) is a central problem in computer science, and advances in SAT-solving algorithms have a far-reaching impact across many fields. Recent works have proposed quantum SAT solvers based on Grover's algorithm, a quantum search technique. However, Grover-based approaches face a key limitation: they typically require prior knowledge of the number of satisfying assignments of the target Boolean formula. This information is unavailable in most practical settings. Quantum counting can be used to estimate this quantity, but it incurs a computational overhead that is several orders of magnitude higher than Grover search. In this paper, we propose a novel quantum SAT solver based on entanglement and equivalence checking. Our method does not assume prior knowledge of the number of solutions and is computationally more efficient than quantum counting. Although the worst case time complexity is inevitably exponential, we prove that the expected time complexity of our approach is only constant time O(1) over random Boolean functions. Experimental results also support our theoretical claim.
Research on quantum computers has gained attention since they are able to solve certain tasks significantly faster than classical machines (in some cases, exponential speed-ups are possible). Since quantum computations typically contain large Boolean components, design automation techniques are required to realize the respective Boolean functions in quantum logic. They usually introduce a significant amount of additional qubits - a highly limited resource. In this work, we propose an alternative method for the realization of Boolean components for quantum logic. In contrast to the current state-of-the-art, we dedicatedly address the main reasons causing the additionally required qubits (namely the number of the most frequently occurring output pattern as well as the number of primary outputs of the function to be realized) and propose to manipulate the function so that both issues are addressed. The resulting methods allow to push the number of required qubits below what is currently considered the minimum.
The verification of quantum circuits is a critical task in quantum computing, ensuring the fidelity and correctness of quantum computations. However, the exponential scaling of the problem with circuit size presents a significant challenge. This paper proposes a novel approach to automated theorem proving for quantum circuit verification by formulating the verification problem as a Boolean satisfiability (SAT) problem. We demonstrate a methodology for translating quantum circuit properties (e.g., output state, gate operations) into equivalent Boolean expressions and subsequently employing existing SAT solvers to determine the satisfiability of these expressions. This approach effectively bridges the gap between quantum circuit theory and SAT solving, offering a potentially scalable solution for verifying complex quantum circuits. The core of our system revolves around a translation module that converts quantum circuit specifications into SAT instances, and a solver interface that interacts with established SAT solvers. We explore the limitations of this approach and discuss future research directions, including hybrid approaches combining SAT solving with quantum simulation techniques. The effectiveness of this method is demonstrated through theoretical analysis and conceptual design, with a focus on the algorithmic efficiency and potential scalability of the proposed framework.
One of the most prominent application areas for quantum computers is solving hard constraint satisfaction and optimization problems. However, detailed analyses of the complexity of standard quantum algorithms have suggested that outperforming classical methods for these problems would require extremely large and powerful quantum computers. The quantum approximate optimization algorithm (QAOA) is designed for near-term quantum computers, yet previous work has shown strong limitations on the ability of QAOA to outperform classical algorithms for optimization problems. Here we instead apply QAOA to hard constraint satisfaction problems, where both classical and quantum algorithms are expected to require exponential time. We analytically characterize the average success probability of QAOA on a constraint satisfaction problem commonly studied using statistical physics methods: random k -SAT at the threshold for satisfiability, as the number of variables n goes to infinity. We complement these theoretical results with numerical experiments on the performance of QAOA for small n , which match the limiting theoretical bounds closely. We then compare QAOA with leading classical solvers. For random 8-SAT, we find that for more than 14 quantum circuit layers, QAOA achieves more efficient scaling than the highest-performance classical solver we tested, WalkSATlm. Our results suggest that near-term quantum algorithms for solving constraint satisfaction problems may outperform their classical counterparts. Published by the American Physical Society 2024