9 papers
Exact Quantum Circuit Optimization is co-NQP-hard
Adam Husted Kjelstrøm, Andreas Pavlogiannis, Jaco van de Pol
As quantum computing resources remain scarce and error rates high, minimizing the resource consumption of quantum circuits is essential for achieving practical quantum advantage. H…
Practical Subarchitectures for Optimal Quantum Layout Synthesis
Kostiantyn V. Milkevych, Jaco van de Pol, Irfansha Shaik
Quantum Layout Synthesis (QLS) maps a logical quantum circuit to a physical quantum platform. Optimal QLS minimizes circuit size and depth, which is essential to reduce the noise o…
Efficient Simulation of High-Level Quantum Gates
Adam Husted Kjelstrøm, Andreas Pavlogiannis, Jaco van de Pol
Quantum circuit simulation is paramount to the verification and optimization of quantum algorithms, and considerable research efforts have been made towards efficient simulators. W…
Depth-Optimal Quantum Layout Synthesis as SAT
Anna B. Jakobsen, Anders B. Clausen, Jaco van de Pol +1
Quantum circuits consist of gates applied to qubits. Current quantum hardware platforms impose connectivity restrictions on binary CX gates. Hence, Layout Synthesis is an important…
Symbolic Model Checking in External Memory
Steffan Christ Sølvsten, Jaco van de Pol
We extend the external memory BDD package Adiar with support for monotone variable substitution. Doing so, it now supports the relational product operation at the heart of symbolic…
CNOT-Optimal Clifford Synthesis as SAT
Irfansha Shaik, Jaco van de Pol
Clifford circuit optimization is an important step in the quantum compilation pipeline. Major compilers employ heuristic approaches. While they are fast, their results are often su…
Optimal Layout-Aware CNOT Circuit Synthesis with Qubit Permutation
Irfansha Shaik, Jaco van de Pol
CNOT optimization plays a significant role in noise reduction for Quantum Circuits. Several heuristic and exact approaches exist for CNOT optimization. In this paper, we investigat…
Optimal Layout Synthesis for Deep Quantum Circuits on NISQ Processors with 100+ Qubits
Irfansha Shaik, Jaco van de Pol
Layout synthesis is mapping a quantum circuit to a quantum processor. SWAP gate insertions are needed for scheduling 2-qubit gates only on connected physical qubits. With the ever-…
Certifying Emptiness of Timed Büchi Automata
Simon Wimmer, Frédéric Herbreteau, Jaco van de Pol
Model checkers for timed automata are widely used to verify safety-critical, real-time systems. State-of-the-art tools achieve scalability by intricate abstractions. We aim at furt…