qSAT: Design of an Efficient Quantum Satisfiability Solver for Hardware Equivalence Checking

• URL: http://arxiv.org/abs/2409.03917v1
• Date: Thu, 5 Sep 2024 21:25:38 GMT
• Title: qSAT: Design of an Efficient Quantum Satisfiability Solver for Hardware Equivalence Checking
• Abstract summary: We have proposed an efficient quantum SAT solver for equivalence checking of circuits employing Grover's algorithm. The Exclusive-Sum-of-Product based generation of the Conjunctive Normal Form equivalent clauses demand less qubits and minimizes the gates and depth of quantum circuit interpretation.
• Score: 2.178037930899554
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The use of Boolean Satisfiability (SAT) solver for hardware verification incurs exponential run-time in several instances. In this work we have proposed an efficient quantum SAT (qSAT) solver for equivalence checking of Boolean circuits employing Grover's algorithm. The Exclusive-Sum-of-Product based generation of the Conjunctive Normal Form equivalent clauses demand less qubits and minimizes the gates and depth of quantum circuit interpretation. The consideration of reference circuits for verification affecting Grover's iterations and quantum resources are also presented as a case study. Experimental results are presented assessing the benefits of the proposed verification approach using open-source Qiskit platform and IBM quantum computer.

Related papers

• Verifiable quantum advantage in extremely low depth [52.51019642214249]
  We give a problem that is solvable by shallow quantum circuits, hard for computation in time under lattice-based assumptions.<n>We prove that shallow quantum circuits have sufficient structure to solve certain classically hard tasks whose solutions can be verified efficiently.
  arXiv  Detail & Related papers  (2026-09-01T15:54:34Z)
• Performance Gains in Quantum SAT Solvers Using ESOP Encoding [1.3267048706241158]
  We investigate an Exclusive-Sum-of-Products-based CNF representation tailored for quantum SAT solving.<n>We derive tighter upper bounds on qubit requirements and Clifford+$T$ gate counts for Grover-based SAT solvers when e-CNF encodings are employed.<n> Experimental evaluation on representative SAT benchmarks demonstrates that the proposed e-CNF-based approach yields substantial and consistent reductions in quantum resources.
  arXiv  Detail & Related papers  (2026-05-15T17:17:07Z)
• Distributed Implementation of Variational Quantum Eigensolver to Solve QUBO Problems [0.0]
  We present a distributed algorithm and implementation of the variational quantum eigensolver (VQE)<n>DVQE enables the execution of parameterized quantum circuits across multiple quantum processing units (QPUs) in a distributed fashion.
  arXiv  Detail & Related papers  (2025-08-24T17:55:07Z)
• YAQQ: Yet Another Quantum Quantizer -- Design Space Exploration of Quantum Gate Sets using Novelty Search [0.9932551365711049]
  We present a software tool for comparative analysis of quantum processing units and control protocols based on their native gates. The developed software, YAQQ (Yet Another Quantum Quantizer), enables the discovery of an optimized set of quantum gates.
  arXiv  Detail & Related papers  (2024-06-25T14:55:35Z)
• Equivalence Checking of Parameterised Quantum Circuits [13.796569260568939]
  We propose a novel compact representation for PQCs based on tensor decision diagrams. We present an algorithm for verifying PQC equivalence without the need for instantiation.
  arXiv  Detail & Related papers  (2024-04-29T06:25:00Z)
• Bayesian Parameterized Quantum Circuit Optimization (BPQCO): A task and hardware-dependent approach [49.89480853499917]
  Variational quantum algorithms (VQA) have emerged as a promising quantum alternative for solving optimization and machine learning problems. In this paper, we experimentally demonstrate the influence of the circuit design on the performance obtained for two classification problems. We also study the degradation of the obtained circuits in the presence of noise when simulating real quantum computers.
  arXiv  Detail & Related papers  (2024-04-17T11:00:12Z)
• Quantum Approximate Optimisation for Not-All-Equal SAT [9.427635404752936]
  We apply variational quantum algorithm QAOA to a variant of satisfiability problem (SAT): Not-All-Equal SAT. We show that while the runtime of both solvers scales exponentially with the problem size, the scaling for QAOA is smaller for large enough circuit depths.
  arXiv  Detail & Related papers  (2024-01-05T15:11:24Z)
• Equivalence Checking of Parameterized Quantum Circuits: Verifying the Compilation of Variational Quantum Algorithms [3.610459670994051]
  Variational quantum algorithms have been introduced as a promising class of quantum-classical hybrid algorithms. It is essential to verify that parameterized quantum circuits have been compiled correctly. No methodology capable of handling circuits with parameters has been proposed yet.
  arXiv  Detail & Related papers  (2022-10-21T18:00:04Z)
• Iterative Qubits Management for Quantum Index Searching in a Hybrid System [56.39703478198019]
  IQuCS aims at index searching and counting in a quantum-classical hybrid system. We implement IQuCS with Qiskit and conduct intensive experiments. Results demonstrate that it reduces qubits consumption by up to 66.2%.
  arXiv  Detail & Related papers  (2022-09-22T21:54:28Z)
• Quantum circuit debugging and sensitivity analysis via local inversions [62.997667081978825]
  We present a technique that pinpoints the sections of a quantum circuit that affect the circuit output the most. We demonstrate the practicality and efficacy of the proposed technique by applying it to example algorithmic circuits implemented on IBM quantum machines.
  arXiv  Detail & Related papers  (2022-04-12T19:39:31Z)
• Circuit Symmetry Verification Mitigates Quantum-Domain Impairments [69.33243249411113]
  We propose circuit-oriented symmetry verification that are capable of verifying the commutativity of quantum circuits without the knowledge of the quantum state. In particular, we propose the Fourier-temporal stabilizer (STS) technique, which generalizes the conventional quantum-domain formalism to circuit-oriented stabilizers.
  arXiv  Detail & Related papers  (2021-12-27T21:15:35Z)
• Quantum circuit architecture search for variational quantum algorithms [88.71725630554758]
  We propose a resource and runtime efficient scheme termed quantum architecture search (QAS) QAS automatically seeks a near-optimal ansatz to balance benefits and side-effects brought by adding more noisy quantum gates. We implement QAS on both the numerical simulator and real quantum hardware, via the IBM cloud, to accomplish data classification and quantum chemistry tasks.
  arXiv  Detail & Related papers  (2020-10-20T12:06:27Z)
• Verifying Results of the IBM Qiskit Quantum Circuit Compilation Flow [7.619626059034881]
  We propose an efficient scheme for quantum circuit equivalence checking. The proposed scheme allows to verify even large circuit instances with tens of thousands of operations within seconds or even less.
  arXiv  Detail & Related papers  (2020-09-04T19:58:53Z)
• QUANTIFY: A framework for resource analysis and design verification of quantum circuits [69.43216268165402]
  QUANTIFY is an open-source framework for the quantitative analysis of quantum circuits. It is based on Google Cirq and is developed with Clifford+T circuits in mind. For benchmarking purposes QUANTIFY includes quantum memory and quantum arithmetic circuits.
  arXiv  Detail & Related papers  (2020-07-21T15:36:25Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.