Finding Photonics Circuits via δ-weakening SMT
summary
A pipeline encodes transfer matrices (bounds in [-1,1], unitarity, Fock-basis action up to amplitude α) into SMT‑LIB and runs delta-weakening SMT/dReal to get δ‑satisfiable matrix bounds, then performs unitary extraction via SVD to produce implementable unitaries. The Python tool reproduces the known post‑selection CZ with success probability 1/9 (optimal), scales to single‑auxiliary wires with up to ~13 photons, provides new Givens‑rotation circuits with two vacuum auxiliaries, and yields weaker/unknown results for heralded schemes. Outputs feed Perceval for circuit diagrams.
AI-written summary · about
chapters (10)
- 0:00Photonic circuits intro
- 10:22Problem statement SMT
- 13:40Delta weakening SMT solvers
- 16:55SMT encoding for circuits
- 19:51Search algorithm extraction
- 20:55Experimental results
- 23:01Testing new gates
- 24:05Heralded measurement feasibility
- 25:07Conclusions future work
- 27:56Q&A
related talks
17mOptimization and Synthesis of Quantum Circuits with Global Gates
19mEquality Saturation for Quantum Circuit Optimization
01h 10mThe Rise & Collapse of a Quantum State
30mSymbolic Execution of Hadamard-Toffoli Quantum Circuits
15mModular Component-Based Quantum Circuit Synthesis
14mHybrid quantum-classical circuit simplification with the ZX-calculus
19mOptimizing Ancilla-Based Quantum Circuits with SPARE
17mQGAT: A Generate-and-Test Paradigm for Quantum Circuits