Finding Photonics Circuits via -weakening SMT
arXiv:2509.11678 · doi:10.1007/978-3-032-15700-3_7
Abstract
For quantum computers based on photonics, one main problem is the synthesis of a photonic circuit that emulates quantum computing gates. The problem requires using photonic components to build a circuit that act like a quantum computing gate with some probability of success. This involves not only finding a circuit that can correctly act like a quantum gate, but also optimizing the probability of success. Whilst many approaches have been given in the past and applied to specific gates, they often lack ease of reusability. We present a tool that uses dReal, a δ-weakening SMT solver, to find such photonic circuits, optimize the likelihood of occurring, and provide some guarantee that the result is optimal. We demonstrate the usage of our tool by recreating known results in the literature, extending upon them, and presenting new results for Givens rotation gates.
arXiv comment20 pages, 5 figures
References in corpus (8)
- Fault-tolerant quantum computation by anyons
- Review article: Linear optical quantum computing
- Linear Optical CNOT Gate in the Coincidence Basis
- A Note on Linear Optics Gates by Post-Selection
- Topological Quantum Compiling
- On photonic controlled phase gates
- symQV: Automated Symbolic Verification of Quantum Programs
- Towards a SAT Encoding for Quantum Circuits: A Journey From Classical Circuits to Clifford Circuits and Beyond