Encoding Circuit Satisfiability in Rydberg Atom Arrays

AI summary

Overview

Research area: Quantum computing hardware and problem encoding — specifically, mapping Boolean circuit satisfiability (Circuit-SAT) onto Rydberg atom arrays operated as maximum-weight independent set (MWIS) solvers.

Technical level: Advanced. The paper assumes familiarity with NP-completeness, graph reductions, Rydberg blockade physics, and VLSI-style placement and routing.

Scope: The paper introduces CAMERA, a gate-level compiler that encodes Boolean circuits directly into weighted king-subgraph (KSG) gadgets on Rydberg atom arrays, bypassing the conventional CNF intermediate, and validates the resulting layouts with exact ground-state calculations and a tensor-network simulation of an annealing protocol.

What This Paper Is About

Rydberg atom arrays naturally solve the maximum-weight independent set problem: atoms placed closer than a blockade radius cannot both be excited, so the array's low-energy configurations correspond to independent sets of the graph formed by atom positions. Circuit-SAT can therefore be run on such hardware, but the standard route goes through a conjunctive normal form (CNF) conversion (the Tseitin transformation), then a conflict graph, then an embedding with auxiliary "quantum wire" atoms — each stage adding atoms that encode the reduction rather than the circuit. The paper's goal is to eliminate that intermediate representation and compile logic gates directly into compact weighted graph gadgets, dramatically reducing the number of atoms needed.

Key Contributions

1. CAMERA, a direct gate-level encoding. A method that represents each Boolean primitive (AND, OR, XOR, NOT, plus fanout and crossing gadgets) as a compact weighted KSG gadget whose maximum-weight independent sets reproduce the gate's truth table exactly, and that composes gadgets by shared-port identification or by weighted atom chains.

2. A satisfiability decision procedure with certification. A "branching" primitive that forces a vertex in or out of the independent set, combined with two theorems: Theorem 1 (the port projections of the MWIS optima are exactly the circuit's truth-table rows) and Theorem 2 (the instance is satisfiable if and only if the branched optimum saturates the bound W* − W_br = w_O, with a strict deficit certifying unsatisfiability).

3. A VLSI-inspired placement-and-routing compiler. A two-stage compiler ("abstract" then "real") using A* routing on an eight-neighbor grid, PathFinder-style history-based rerouting, simulated annealing over placements, and parity-aware wire repair — with a "clean edge condition" that rejects layouts containing unintended blockade interactions.

4. Forward evaluation and general constraint queries. Branching on input ports instead of the output turns the same compiled graph into a forward circuit evaluator; pinning an arbitrary subset of ports answers general constraint queries, with the SAT decision and forward evaluation as the two extreme cases.

Main Findings

• Atom cost reduction of 22.4 ± 1.8 on average. On random benchmark circuits of 3 to 8 gates (100 random circuits per gate count on each route), the direct gadget route lowers atom cost relative to the CNF route by an average factor of 22.4 ± 1.8, with the median CNF-to-gadget ratio ranging from 19.5 to 23.8 across the window.
• Gadget medians grow from 35 to 142 atoms. Over the same 3–8 gate window, CNF medians follow 51.1 g² and climb to nearly 3000 atoms by eight gates, while gadget medians grow monotonically from 35 to only 142 atoms. The 21× median suppression is marked at eight gates.
• Quadratic coefficients differ by more than twentyfold. Both routes share the same NP-hardness-imposed quadratic worst case, but forcing the quadratic form through the gadget medians yields a coefficient of 2.29 versus 51.1 for CNF (R² = 0.96 versus 0.94). The paper notes that over so narrow a window the gadget medians remain nearly as consistent with linear growth.
• About 95% fewer atoms, roughly twentyfold, on the random benchmark. For the full adder and multiplier, the reduction is about thirtyfold.
• Complete truth-table verification of composed circuits. Exact classical ground-state calculations verify a 30-atom three-gate instance, an 85-atom full adder, and a 165-atom two-bit multiplier against their complete truth tables.
• End-to-end solution of a 30-atom instance. For C(I₁,I₂,I₃) = (I₁ ∧ I₂) ⊕ (I₂ ∨ I₃), the compiled graph has 30 atoms and 41 edges, with optimal weight W* = 23 across eight degenerate optima. Output branching deletes three framed atoms to leave a 27-atom branched graph with W_br = 22, giving W* − W_br = 1 = w_O and thereby certifying satisfiability.
• 58.0% of projective samples reach the target manifold. A closed-system tensor-network simulation of the 30-atom instance under a 4 μs neutral-atom annealing schedule reached W* = 23 in 58.0% of 1000 projective samples (988 blockade-consistent), and W_br = 22 in 54.6% of the branched-graph samples (986 blockade-consistent).
• Only two detuning values are ever needed. Because library weights are 1 and 2 and every identified pin joins a weight-1 gadget port to a weight-1 chain endpoint, no rule raises an atom above weight 2; the binary alphabet w ∈ {1,2} is preserved under composition however large the circuit.
• The CNF route is already expensive at three gates. For the same three-gate circuit, the CNF chain produces an intermediate MIS graph of 30 vertices — already as many as the entire gadget compilation — before the wire-chain embedding inflates it further.

Methodology in Plain English

The approach has four moving parts.

Gadgets. For each logic gate, the authors search by brute force over small clusters of atoms on an integer grid (the king-subgraph geometry, where two sites are adjacent when their Chebyshev distance is at most one). Candidate clusters get small integer weights, and a cluster is accepted only if its maximum-weight independent sets, read off at designated "port" atoms, reproduce the gate's truth table. This yields an auditable library — 6-atom AND, 6-atom OR, 9-atom XOR, 5-atom fanout, and a two-atom NOT — rather than a heuristic design.

Composition. Gates are wired together by identifying an output port with a downstream input port (summing their weights) or by joining them with a chain of wire atoms. A "clean edge condition" must hold: the composite graph has no edges beyond those inside the gadgets and chains.

Compilation. Wiring that cannot be realized by direct adjacency is routed as wire chains, and crossings become explicit crossing gadgets. An abstract stage places gadget "anchors" on a coarse grid and routes pins with A*, resolving ordering conflicts via history-based rerouting; an ensemble of simulated-annealing runs collects valid layouts, which are then compacted greedily. A real stage expands the grid until rigid gadget templates fit, re-routes split nets, repairs even-parity routes, and assigns weights.

Readout. To decide satisfiability, pin the output to 1 by deleting its closed neighborhood from the graph and crediting its weight. Since the reference optimum W* is simply the sum of the fixed gadget and wire-chain optima, no separate optimization is needed; one MWIS computation on the branched graph suffices. If the branched optimum plus the output weight equals W*, the instance is satisfiable and the input port occupations from that same computation give the witness; a strict deficit proves unsatisfiability. Branching on inputs instead evaluates the circuit forward on a given assignment.

Why This Matters

The paper reframes problem encoding as a physical design task rather than a software afterthought: a reduction that is polynomial in theory can still be ruinously expensive in atoms, wires, and site-resolved control. By keeping the circuit's directed-acyclic-graph structure available throughout placement and routing, CAMERA shows that a structured source problem can stay structured on the device.

Real-world applications include:

• Combinational equivalence checking in electronic design automation, framed in the paper as a "miter" comparing two circuits A and B through an XOR gate whose output is 1 exactly when they differ.
• Formal hardware verification more broadly, since Circuit-SAT is the underlying NP-complete decision problem.
• Combinatorial optimization on neutral-atom hardware, through the native MWIS mapping with site-dependent detunings realized as local light shifts.
• Compiling other structured discrete problems — the authors position the gadget-and-routing workflow as a template for a broader family of encodings onto Rydberg arrays.

Industry relevance: the more-than-twentyfold atom saving matters directly for neutral-atom hardware, where platforms have scaled from 51-atom chains to tweezer registers of more than six thousand atoms. Fewer atoms per logical problem means larger practical instances fit on existing machines, and the restriction to two local-detuning values simplifies the control hardware required.

Future Directions

• Closing the gap between simulation and experiment. The annealing results come from a closed-system tensor-network simulation of a 30-atom instance; the paper does not report an experimental demonstration, leaving open how decoherence, atom-position disorder, and calibration error affect the 58.0% success rate on hardware.
• Scaling the compiler to larger arithmetic and industrial circuits. Verified compilations stop at an 85-atom full adder and a 165-atom two-bit multiplier; whether the placement-and-routing pipeline remains tractable and compact for realistic netlists with dense fanout and many crossings is untested.
• Reducing routing overhead further. Even the gadget route must realize every crossing through an explicit crossing gadget, so worst-case wiring forces a quadratic atom cost with a coefficient of 2.29; better crossing structures or routing strategies could lower this prefactor.
• Extending to broader constraint queries and other problem families. The framework for pinning arbitrary port subsets is general, and the authors propose the gadget-plus-compiler workflow as a route toward a wider family of combinatorial problems — but only Circuit-SAT instances are demonstrated here.

Target Audience

Researchers and engineers working on neutral-atom quantum computing and quantum optimization, especially those interested in hardware-native problem encodings, gadget-based reductions, and the interface between EDA-style compilation and quantum device constraints. It will also suit theoretical computer scientists studying reductions to maximum independent set on geometric graphs, and quantum algorithm practitioners who want a concrete, verified worked example of an end-to-end encode-solve-readout pipeline. Readers without a background in NP-completeness or Rydberg blockade physics will find the material demanding.

Authors’ abstract

Rydberg atom arrays natively encode the maximum-weight independent set (MWIS) problem through the blockade mechanism, so the Boolean circuit satisfiability problem (Circuit-SAT) can be brought onto the platform once it is reduced to MWIS. The conventional encoding of Circuit-SAT in the Rydberg atom array proceeds through conjunctive normal form (CNF) and incurs a substantial atom overhead. We introduce CAMERA (Circuit-SAT Atom-efficient MWIS Encoding for Rydberg Arrays), a method that provides MWIS encodings of Circuit-SAT instances on the king subgraph geometry of the array. CAMERA represents each logic gate as a compact weighted gadget and assembles the gadgets with a placement and routing compiler inspired by very large scale integration (VLSI) design. On random multi-gate benchmarks, the direct encoding route lowers the atom cost relative to the CNF route by an average factor of $22.4 \pm 1.8$. To demonstrate that the encoding extends from individual weighted gadgets to multi-gate arithmetic blocks, we compile a full adder and a multiplier, verifying each against its complete truth table by exact classical ground state calculations. We further showcase solving a representative Circuit-SAT instance end-to-end, from gate level compilation through a closed-system tensor-network simulation of a hardware-compatible annealing protocol on the encoded 30-atom instance to readout of a satisfying assignment. These results establish a complete encoding and simulation workflow as a proof of principle, and a concrete route toward solving a broader family of combinatorial problems on Rydberg atom arrays.