Technical Summary: Finding Photonics Circuits via $\delta$-weakening SMT

Problem Statement

The paper addresses the synthesis of photonic circuits capable of emulating quantum computing gates using linear optics. In linear optical quantum computing (LOQC), quantum gates are implemented using basic building blocks such as beam splitters, phase shifters, and detectors. A fundamental challenge in this domain is that a single quantum gate can be represented by numerous circuit configurations, each with a specific probability of success and a probability of acting in an undesired manner.

The core problem is defined as Problem 3: Given a target unitary quantum operation $U$ acting on $q$ qubits, a specific number of optical wires ($2q + m_a$, where $m_a$ represents auxiliary wires), and a coincidence basis $C$, find a transfer matrix $\hat{U}$ for a dual-rail optical operation that maximizes the probability of success ($|\alpha|^2$). The solution must ensure that the action of $\hat{U}$ on the relevant subspace of the Fock space (the coincidence basis) mimics $U$ up to a complex scaling factor $\alpha$.

The authors distinguish between two measurement regimes:

1. Post-selection: All wires are measured, and only outcomes matching the quantum computational basis are accepted.
2. Heralded selection: Only auxiliary wires are measured; if they return to their initial state (e.g., vacuum), the operation is considered successful, allowing the qubit state to be reused.

Methodology

Encoding into Non-Linear Real Arithmetic (NRA)

The authors transform the synthesis problem into a constraint satisfaction problem within Non-Linear Real Arithmetic (NRA). The transfer matrix $\hat{U}$ and the success amplitude $\alpha$ are modeled as real variables (though the paper notes complex variables can be encoded as pairs of real variables).

The constraints are formulated as follows:

• Unitarity: $\hat{U}$ must be a unitary matrix ($\hat{U}\hat{U}^\dagger = I$). This generates quadratic polynomial constraints.
• Bounds: Variables are restricted to the range $[-1, 1]$.
• Fock Space Equivalence: The core constraint requires that the action of $\hat{U}$ on the Fock basis states (specifically the coincidence basis $C$) equals the target operation $U$ scaled by $\alpha$. This results in polynomial constraints of degree $k$, where $k$ depends on the number of photons used in the circuit.

$\delta$-Weakening and dReal

Standard SMT solvers struggle with the undecidability of general NRA, particularly when high-degree polynomials are involved. The authors utilize $\delta$-weakening, a technique implemented in the solver dReal. Instead of requiring exact equality ($f(x) = 0$), $\delta$-weakening allows for a small perturbation ($|f(x)| \le \delta$).

• If a solution exists within the tolerance $\delta$, dReal returns a region of values ($\delta$-sat).
• This approach allows the solver to find approximate solutions much faster than standard solvers, which might fail to find any solution or take excessive time.

Search Algorithm and Refinement

The synthesis process employs an iterative search algorithm (Algorithm 1):

1. Iterative Optimization: The algorithm starts with a minimum success threshold $\alpha_{min}$. It queries dReal to find a transfer matrix satisfying the constraints with a success probability greater than $\alpha_{min}$.
2. Threshold Update: If a solution is found, $\alpha_{min}$ is updated to slightly exceed the upper bound of the found probability, and the search repeats.
3. Termination: The loop continues until a timeout occurs or the solver returns "unsat" (no solution exists above the current threshold).
4. Exact Recovery: Since dReal returns a region of approximate values, the authors apply Singular Value Decomposition (SVD) to a matrix within this region. By replacing the singular values with 1, they construct a strictly unitary matrix. They then compare the resulting matrices against the target $U$ to select the best candidate, effectively converting the $\delta$-approximation into an exact, implementable transfer matrix.

Key Contributions

1. Novel Synthesis Technique: The paper introduces the first application of $\delta$-weakening SMT solvers to the synthesis of linear optical circuits. This approach differs from previous decomposition schemes or computational simplification tools by treating the circuit design as a global optimization problem.
2. Automation and Generality: The tool is fully automated; users input a target gate and circuit setup (wires, photons), and the system searches for the optimal transfer matrix without requiring manual derivation of circuit structures.
3. Handling Approximations: The authors provide a rigorous method to bridge the gap between the approximate solutions provided by $\delta$-SMT solvers and the exact unitary matrices required for physical implementation, using SVD refinement.
4. Complex Variable Encoding: The paper discusses the theoretical possibility of encoding complex variables (essential for general quantum gates) as pairs of real variables, acknowledging the resulting increase in computational complexity.

Results

The tool was validated against known literature results and used to explore new configurations:

• Post-Selection Results:

  • Verification: The tool successfully verified known infeasibility results (e.g., CZ gates are impossible with 0 or 1 auxiliary vacuum wires) and reproduced known optimal circuits (e.g., CZ with 2 vacuum wires achieving $1/9$ success probability).
  • Auxiliary Wire Exploration: The authors investigated synthesizing CZ gates using a single auxiliary wire with varying numbers of photons. Results mirrored previous findings, showing that success probability generally decreases as the number of photons increases beyond one.
  • Givens Rotations: The tool synthesized circuits for Givens rotation gates (universal for quantum chemistry). It found that for certain angles (e.g., $\theta = \pi/2$), success probabilities of $1/9$ could be achieved. The data suggested a relationship between the rotation angle and the maximum achievable success probability, with a minimum near $\theta \approx 0.5$.

• Heralded Results:

  • The tool confirmed the infeasibility of certain heralded setups (e.g., CZ with 0 or 1 vacuum wires).
  • However, the tool frequently returned "unknown" (due to timeouts) when attempting to find known heralded solutions (e.g., CZ with two ancillary wires containing one photon each). The authors attribute this to the increased degree of polynomials and the sheer number of equations required, which pushes current SMT solvers to their limits.

Significance and Limitations

Significance:
The paper demonstrates that SMT-based synthesis is a viable and powerful method for designing photonic circuits, capable of both reproducing known results and discovering new configurations (such as for Givens rotations). The technique is particularly effective for post-selected schemes where polynomial degrees remain manageable. The authors suggest that photonic circuits for quantum chemistry (using Givens rotations) may be more feasible to synthesize optimally than general quantum computing gates due to the specific structure of the required operations.

Limitations and Future Work:
The authors are modest regarding the current scope:

• Heralded Schemes: The technique currently hits a "wall" when applied to heralded selection, primarily due to the high degree of polynomials involved.
• Complex Variables: While theoretically possible, encoding complex variables doubles the number of variables and constraints, significantly increasing computation time. Finding solutions for multi-qubit gates with complex phases remains out of reach for current tools.
• Scalability: The method struggles with gates acting on 3 or more qubits (e.g., Toffoli gates) due to the explosion in the number of constraints.

The paper concludes that advancing this field requires developments in SMT solving, specifically techniques for handling bounded-degree polynomials in NRA or efficient solvers for Complex Arithmetic (CA) theories.