QuPRS: Quantum Path-sum Reduction and Solver

QuPRS("kyu-parse") is a tool for Quantum Circuit tool integrate Path-sum Reduction and Solver.

In quantum computing, verifying whether an optimized or compiled quantum circuit is functionally equivalent to the original circuit is a crucial task. QuPRS aims to solve this problem, and its features include:

• Novel verification method: Based on pathsum, which is a circuit representation method different from traditional matrix products.
• Multiple verification strategies:
  1. Hybrid mode (RR + WMC): Combines the efficiency of reduction rules and the completeness of weighted model counting.
  2. Reduction rules only (RR): Extremely fast, suitable for circuits that can be simplified by local rules.
  3. WMC only: A powerful SAT-based method for more complex circuit structures.
• Seamless integration with Qiskit ecosystem: Circuits can be directly loaded from Qiskit QuantumCircuit objects or QASM files.

Contents

• QuPRS: Quantum Path-sum Reduction and Solver
  • Contents
  • Installation
    • Platform Support
  • Using QuPRS
    • Create pathsum Circuit
    • Import From qasm
  • Equivalence Checking
    • Circuit Prepare
    • Run Equivalence Checking
  • Cite
  • License Information
  • Acknowledgements

Installation

It is recommended to install QuPRS in a virtual environment.

1. Create and activate a Conda virtual environment:

   conda create --name QuPRS python=3.12 # Or your preferred Python version
   conda activate QuPRS
   

2. Install QuPRS using pip:

   pip install QuPRS
   

Platform Support

QuPRS provides pre-built wheels for the following operating systems and architectures:

Using QuPRS

This tool can build quantum circuit using path-sum formulation.

First, import the necessary components from the QuPRS library.

from QuPRS.pathsum import PathSum

Create pathsum Circuit

Create a pathsum Circuit You can create a PathSum.QuantumCircuit object directly:

qubit_num = 2
circuit = PathSum.QuantumCircuit(qubit_num)
circuit = circuit.h(0) # Apply Hadamard gate to qubit 0
circuit = circuit.h(0) # Apply Hadamard gate to qubit 0 again (H*H = I)
# Add more gates as needed
# e.g., circuit = circuit.cx(0, 1)

Import From qasm

pathsum supports importing circuits from QASM files or strings.

From a QASM file:

filename = "my_circuit.qasm"
# Ensure my_circuit.qasm exists and contains valid QASM code
# Example my_circuit.qasm:
# OPENQASM 2.0;
# include "qelib1.inc";
# qreg q[2];
# h q[0];
# cx q[0],q[1];

circuit = PathSum.load_from_qasm_file(filename)

Or

qasm_str = """
OPENQASM 2.0;
include "qelib1.inc";
qreg q[2];
h q[0];
cx q[0],q[1];
"""
circuit = PathSum.load_from_qasm_str(qasm_str)

Equivalence Checking

QuPRS provides tools for checking the equivalence of two quantum circuits, potentially imported from Qiskit or QASM files.

Importing Circuits for Equivalence Checking You can load circuits from QASM files or define them directly using Qiskit for comparison.

Circuit Prepare

• Load from QASM files

  # Assuming circuit1.qasm and circuit2.qasm exist
  from QuPRS.interface.load_qiskit import load_circuit
  
  circuit1 = load_circuit("circuit1.qasm")
  circuit2 = load_circuit("circuit2.qasm")
  

• Direct import from Qiskit QuantumCircuit objects:

  from qiskit import QuantumCircuit 
  
  # Define circuit1 using Qiskit
  circuit1 = QuantumCircuit(2)
  circuit1.h(1)
  circuit1.cx(0, 1)
  circuit1.h(1)
  
  # Define circuit2 using Qiskit
  circuit2 = QuantumCircuit(2)
  circuit2.cz(0, 1)
  

Run Equivalence Checking

• Hybrid: Reduction Rules (RR) and Weighted Model Counting (WMC)

  This method combines RR with WMC for equivalence checking.

  from QuPRS import check_equivalence
  
  result = check_equivalence(circuit1, circuit2, method = "hybrid",)
  

• Using Reduction Rules (RR)

  from QuPRS import check_equivalence
  
  result = check_equivalence(circuit1, circuit2, method = "reduction_rules",)
  

• WMC only (without RR)

  To perform equivalence checking using only WMC, you need to disable the Reduction Rules switch.

  from QuPRS import check_equivalence
  
  result = check_equivalence(circuit1, circuit2, method = "wmc_only",)
  

Cite

If you use QuPRS in your research, please cite our paper:

Equivalence Checking of Quantum Circuits via Path-Sum and Weighted Model Counting
Wei-Jia Huang, Christophe Chareton, Yu-Fang Chen, Kai-Min Chung, Min-Hsiu Hsieh, Alfons Laarman, and Jingyi Mei.
In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2026), Lecture Notes in Computer Science, vol. 15668, pp. 419–439. Springer, 2026.
DOI: 10.1007/978-3-032-22749-2_21

@inproceedings{huang2026equivalence,
  author    = {Huang, Wei-Jia and Chareton, Christophe and Chen, Yu-Fang and Chung, Kai-Min and Hsieh, Min-Hsiu and Laarman, Alfons and Mei, Jingyi},
  title     = {Equivalence Checking of Quantum Circuits via Path-Sum and Weighted Model Counting},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2026)},
  series    = {Lecture Notes in Computer Science},
  pages     = {419--439},
  year      = {2026},
  publisher = {Springer Nature Switzerland},
  doi       = {10.1007/978-3-032-22749-2_21},
  url       = {https://doi.org/10.1007/978-3-032-22749-2_21}
}

You can also cite this software repository via Zenodo:

Floating weighted counts

Ganak 2.8.0 uses --mode=6; GPMC uses -mode=1. Both operate on floating-point encodings of the path sum. Ganak mode 6 prints rounded complex counts (nine significant digits in the pinned release). Neither solver is an exact-arithmetic certificate for the original circuit. Ganak's pinned version, archive/executable SHA256 and architecture checks still apply.

Count fixtures compare against hand-computed complex sums and the other solver using relative error 1e-8 and absolute error 1e-12; individual Rust solver-integration fixtures use a documented 2e-9 absolute budget. These are fixture budgets, not universal error bounds under cancellation. Rust serializes both solver inputs with 17 significant decimal digits in scientific notation (enough to round-trip binary64 weights). Python evaluates symbolic weights at 113 bits where supported and writes their decimal form without an arbitrary nine-decimal quantization. Input precision cannot exceed the information in the original circuit parameters or the numerical type used upstream.

Both Python and Rust WMC backends classify the unrounded, normalized complex count using 1e-6 magnitude and phase thresholds. Python exposes these as config.WMC_MAGNITUDE_TOLERANCE and config.WMC_PHASE_TOLERANCE; config.TOLERANCE remains the independent symbolic-reduction tolerance (default 1e-10). Nonzero global phase gives equivalent* when the count magnitude passes the threshold. Python uses a scaled log-magnitude and signed atan2, avoiding overflow, zero-count division, and negative phases wrapping to nearly 2*pi. Results closer to a decision boundary than encoding or printed-count error should be checked independently; agreement between two solvers alone does not establish exact equivalence. Nonzero exits, crashes, missing results and malformed/non-finite counts are failures, without cross-solver fallback.

Python WMC precision profiling

Use the deterministic microbenchmark to compare 53-bit and 113-bit phase weight evaluation on the same machine:

python scripts/profile_wmc_weight_precision.py --samples 96 --repeats 5 --warmups 2 --json-file python_wmc_precision_profile.json

Its JSON report includes distinct and repeated phases, normalized timing, and platform metadata. Cache timings are experimental only, not enabled in production. The PR benchmark workflow records the report as an artifact. Absolute timings across different CI runners are not directly comparable. This profile is observational and does not introduce a new release gate.

License Information

• The original source code of this project is licensed under the MIT License.

• This project utilizes and depends on several third-party components and libraries, which are governed by their own licenses. For detailed copyright notices and the full license texts of these components, please see the NOTICE.md file.

Acknowledgements

This project utilizes gpmc, a binary component developed by Kenji Hashimoto, for parts of its Weighted Model Counting functionality.