{"id":"2b93fc44-2ce3-4929-911d-db93ea6a3124","arxiv_id":"2608.12938","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":7,"one_line_summary":"A gate-level compiler maps Boolean circuits to weighted king-subgraph MWIS instances on Rydberg arrays, cutting atom counts by about 22x versus CNF-based encoding.","lead":"This paper presents CAMERA, a method that encodes Boolean circuits directly as maximum-weight independent set problems on Rydberg atom arrays, avoiding the atom-heavy CNF intermediate. It reports atom savings of roughly 20 times versus the CNF route and verifies compiled full adders and multipliers by exact ground-state enumeration.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Simulation does not test residual van der Waals interactions, so the hard-blockade assumption is unvalidated for the practical claim.","rationale":"The reader's weakest_assumption is the hard-blockade hardware limit, which is the same concern I identify; I agree with the reader, and add one sharper point: the paper's tensor-network validation does not document its interaction model, so it does not currently discharge the assumption. I find no internal inconsistency in Theorems 1-2 or the gadget library; the exact enumerations are strong evidence for the graph-level claim. The resource-comparison issue (unspecified benchmark generator, no code or data) is also real, but it affects the quantitative atom-count advantage rather than the existence of the encoding; the hard-blockade concern affects whether the encoding is physically realizable, so it is the more load-bearing issue. The verdict should remain CONDITIONAL: the graph-theoretic core is sound, but the hardware claim is conditional on the hard-blockade limit and on documented validation of residual interactions.","tokens_in":35497,"tokens_out":22885,"duration_ms":228675,"concrete_test":"Re-run the Sec. IV D closed-system tensor-network simulation of the compiled 30-atom instance and its 27-atom branched graph with the full van der Waals interaction V_ij = C6/|r_i - r_j|^6 for all pairs, without a hard-blockade truncation, using the stated Aquila-like C6 and lattice spacing and the same pulse schedule. Decode the port atoms of the simulated final states and check whether samples still concentrate on the truth-table rows (W* = 23 and W_br = 22) and whether the Eq. (5) criterion still holds. Also compute the energy of the strongest spurious port projection under the full Hamiltonian and compare it with the MWIS energy; if the spurious state is lower-lying or the decoding fidelity drops appreciably, the hard-blockade assumption is load-bearing and the practical claim must be qualified.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The graph-theoretic core is well supported: Theorem 1 (Eq. 4) and Theorem 2 (Eq. 5) are proved for clean compiled king subgraphs, and exact enumeration on the 30-, 85-, and 165-atom instances confirms the port-projection equality. The load-bearing step is the physical mapping in Sec. II B: in the hard-blockade limit the Rydberg ground state is the MWIS of the compiled graph, but the actual Hamiltonian has a van der Waals tail V_ij = C6/d^6 for all pairs. The compiled graphs have only a unit-weight spectral gap between correct and incorrect port projections; residual interactions between next-nearest neighbors (about 1/64 of the nearest-neighbor interaction for distance ratio 2) can shift energies by more than one weight unit and make a spurious row the ground state, breaking Eq. (4) on real hardware. The only dynamical validation, the tensor-network annealing of Sec. IV D, does not state whether the simulated Hamiltonian included the full C6 tail or truncated interactions at the blockade radius. If truncated, the 58% success gives no evidence about the real-device correspondence; if included, one 30-atom instance is still too narrow to establish robustness across the compiled family. This is load-bearing because the central practical claim of the paper is solving Circuit-SAT on Rydberg arrays, which requires the physical ground state to be the MWIS of the compiled king graph.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces CAMERA, a compiler that maps gate-level Boolean circuits to maximum-weight independent set (MWIS) problems on king-subgraph geometries suitable for Rydberg atom arrays. Each logic gate and routing primitive is represented by a small weighted gadget, and gadgets are composed through clean pin amalgamations. The main theorems state that the port projections of the MWIS manifold of the compiled graph coincide with the circuit truth table (Eq. 4), and that branching the output port gives a satisfiability criterion based on comparing the branched optimum with the reference weight (Eq. 5). The authors validate the construction by exact ground-state enumeration of a 30-atom three-gate circuit, an 85-atom full adder, and a 165-atom two-bit multiplier; benchmark atom counts against a CNF-mediated encoding; and simulate a 4-microsecond annealing protocol for the 30-atom instance.","tokens_in":35795,"tokens_out":9095,"duration_ms":98175,"significance":"If the encoding and the physical mapping hold, this is a useful and well-structured reduction: it preserves circuit topology, uses only two detuning values, yields a parameter-free reference weight, and reduces atom overhead substantially relative to the CNF route. The paper's strengths are the composition-theoretic proofs in the Supplemental Material, the exact exhaustive verification of all compiled instances against their complete truth tables, and the explicit unit-weight gaps that exclude incorrect port projections. The main limitations are that the placement-and-routing compiler is heuristic, the physical correspondence to Rydberg hardware is asserted only in the hard-blockade limit, and the annealing simulation does not specify whether residual van der Waals interactions were included. These issues are local and addressable, but they affect the strength of the practical claims.","major_comments":[{"comment":"The paper's practical claim requires the Rydberg ground state to be exactly the MWIS of the compiled king graph, but this correspondence is established only in the hard-blockade limit. The compiled instances have a unit weight gap between correct and incorrect port projections (Supplemental Tables S2 and S4), while the physical Hamiltonian retains a van der Waals tail V_ij = C6/d^6 for all pairs. Residual interactions beyond the nominal blockade radius can shift energies by an amount comparable to one weight unit when the nearest-neighbor interaction is chosen large enough to enforce blockade, so they can in principle select a spurious port projection and break Eq. (4) on real hardware. The tensor-network annealing simulation of Sec. IV D does not state whether the simulated Hamiltonian included the full C6 tail or truncated interactions at the blockade radius; if it truncated, the 58% success rate gives no evidence about residual-tail robustness, and if it included the tail, a single 30-atom instance is too narrow a test. I ask the authors to simulate the three compiled instances with the full interaction tail, report the resulting gap between the correct and spurious manifolds, and either quantify the robustness of the encoding or restrict the hardware-facing claims accordingly.","section":"Sec. III C; Algorithms S2-S3"},{"comment":"Theorem 1 is conditional on the compiler producing a layout that satisfies the clean edge condition, but the placement-and-routing pipeline of Sec. III C is a heuristic search (simulated annealing, A* routing, PathFinder rerouting, and greedy descent) with no termination or completeness guarantee. The paper presents CAMERA as an automatic route from a gate-level netlist to a blockade-valid layout, so the absence of any characterization of compilation success is load-bearing for the claimed generality. Please add either a completeness/termination result for a suitable class of circuits, or an explicit statement that the compiler is heuristic together with empirical success statistics on a larger set of netlists.","section":"Sec. III C; Algorithms S2-S3"}],"minor_comments":[{"comment":"The sentence 'The clean edge condition of Sec.S4' contains a broken cross-reference; it should refer to Definition S4 or Section SI of the Supplemental Material.","section":"Sec. III C"},{"comment":"The phrase 'combinational equivalence checking by amiter' should read 'by a miter'.","section":"Fig. 1 caption"},{"comment":"The two quadratic fits are based on only six median values each, and the text itself notes that the gadget medians are nearly as consistent with linear growth; the coefficient comparison (2.29 versus 51.1) should be presented as an empirical description of the sampled window rather than as a structural scaling law.","section":"Sec. IV A"},{"comment":"The tensor-network simulation should report its numerical parameters, including bond dimension, time step, and truncation error, and should state explicitly whether the full van der Waals tail was included in the simulated Hamiltonian.","section":"Sec. IV D"},{"comment":"The exact enumeration of the 85- and 165-atom graphs by a column-transfer dynamic program is mentioned but not described; please provide the method details or release the code so that the reported counts and gap values can be reproduced.","section":"Supplemental Secs. SVI-SVII"}],"recommendation":"major_revision","confidential_remarks":"The graph-theoretic core is sound and the manuscript is likely publishable after revision. The main risk is that the physical-hardware validation is weaker than the abstract implies; I would recommend that the authors either perform full-tail interaction simulations or temper the claims about executing these instances on current weighted-MIS platforms."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The core of this paper is the composition theory. The authors prove that clean amalgamation of weighted KSG gadgets realizes the circuit truth table exactly, and that output branching decides satisfiability with a one-weight-unit criterion. That is real: the proofs in the supplement are constructive, and the 30-, 85-, and 165-atom instances are all verified by exhaustive ground-state enumeration, including gapped exclusion of wrong port projections. I read the central claim as holding up: the MWIS manifold of the compiled graph is the truth table of the circuit. That is a solid, useful result for anyone working on Rydberg encodings of structured combinatorial problems.\n\nThe gadget library itself is carefully done. The brute-force polyplet enumeration with minimality certificates gives real confidence that the AND, OR, XOR, crossing, and fan-out gadgets are not ad hoc. The binary weight alphabet surviving composition is a nice practical property. The VLSI-style router is a plausible engineering solution, and the 22.4x atom-count reduction over the CNF route is directionally credible, even though the random benchmark generator is unspecified and no code or data are provided. The latter is a genuine gap: the paper's headline number is not independently reproducible as submitted.\n\nThe soft spots are proportionate. The hard-blockade assumption is the one I would want the authors to address head-on. The Hamiltonian has a C6/d^6 tail, and the compiled graphs have only unit-weight spectral gaps. The tensor-network annealing simulation, as reported, does not state whether the tail was included or truncated, and one 30-atom instance is too narrow to establish robustness. That does not sink the graph-theoretic result, but it does mean the practical claim \"ready for current hardware\" is not yet supported. The compiler's heuristic nature and the lack of termination guarantees for validation are minor by comparison.\n\nWho is this for? Researchers working on encoding combinatorial problems into Rydberg MWIS, and anyone interested in gadget-based quantum optimization. It deserves a serious referee. I would engage with it, and I would want the supplementary material and gadget specifications accessible for reuse.","headline":"A genuinely new gate-level compiler from Circuit-SAT to weighted king-subgraph MWIS, with a proved composition theorem and exact ground-state verification on three sizes; the genuine soft spots are missing code/data and an unvalidated hard-blockade assumption in the annealing simulation.","tokens_in":36318,"tokens_out":852,"would_cite":true,"duration_ms":11612,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Circuit-SAT maps straight to Rydberg atoms, cutting atom cost 22-fold.","keywords":["Circuit-SAT","Rydberg atom arrays","maximum weight independent set","king subgraph","gadget encoding","VLSI placement and routing","quantum annealing","combinational equivalence checking"],"falsifier":"Compile a known satisfiable and a known unsatisfiable circuit, branch the output port, and run exact classical MWIS on both the full and branched graphs: if any maximum-weight independent set of the full graph projects to a row outside the circuit truth table, or if satisfiable instances fail to satisfy $W^{\\star} - W_{\\mathrm{br}} = w_O$ while unsatisfiable instances satisfy it, Theorem 1 falls. A hardware test would measure the final-state weight distribution after the 4$\\mu$s pulse on the 30-atom layout and check whether the most probable weight is $W^{\\star}=23$ for the full graph and $W_{\\mathrm{br}}=22$ for the branched graph; a systematic shortfall would indicate residual interactions or detuning errors beyond the hard-blockade model.","tokens_in":35326,"feed_emoji":"⚛️","tokens_out":7640,"duration_ms":66412,"temperature":0.7,"pith_summary":"This paper tries to establish that Boolean circuit satisfiability can be encoded natively on a Rydberg atom array without the usual intermediate step of a conjunctive normal form formula. The proposed compilation, CAMERA, replaces each logic gate with a small weighted king-subgraph gadget, routes wires with a VLSI-style placement and routing compiler, and proves that the maximum-weight independent sets of the resulting graph project exactly onto the rows of the circuit truth table. The atom-count payoff is large: across random circuits of three to eight gates the direct encoding uses, on average, $22.4 \\pm 1.8$ times fewer atoms than the CNF-mediated route, and exact ground-state checks on an 85-atom full adder and a 165-atom two-bit multiplier reproduce their complete truth tables. If the construction holds up, Rydberg arrays become reconfigurable logic blocks that can decide a Circuit-SAT instance with one weighted independent-set optimization on a branched graph.","feed_headline":"Circuit-SAT maps straight to Rydberg atoms, cutting atom cost 22-fold","feed_subtitle":"Gate-level compiler replaces thousands of atoms with dozens by skipping CNF.","key_machinery":"The load-bearing object is the weighted king-subgraph gadget: a small cluster of atoms with weights in $\\{1,2\\}$ whose maximum-weight independent sets realize the truth table of a Boolean primitive. The library contains AND, OR, NOT, XOR gates plus fan-out, crossing, and variable-length wire gadgets, all found by an automated exhaustive search and certified minimal within the searched class. Composition happens through clean pin amalgamation, meaning identified pins sum their weights and no unintended edges are introduced; Theorem 1 shows this preserves the truth relation exactly. The branching primitive, which pins a bit by deleting either the vertex to force 0 or its closed neighborhood to force 1, is the operation that turns the graph into a SAT decider. A placement-and-routing compiler using history-based rerouting and simulated annealing on a king grid produces blockade-valid layouts while keeping every atom weight in $\\{1,2\\}$, so only two local detuning values are needed.","core_discovery":"The paper's central claim is that the MWIS manifold of the compiled weighted king subgraph is the truth table of the circuit: port projections of the maximum-weight independent sets are exactly the rows $(x, F_C(x))$ of the circuit (Eq. 4), and the optimal weight is the sum of the constituent gadget optima. Deciding satisfiability then reduces to one branching operation: deleting the output port and the atoms it blockades, solving the MWIS on the reduced graph, and comparing the branched optimum $W_{\\mathrm{br}}$ with the reference $W^{\\star}$; the instance is satisfiable exactly when $W^{\\star} - W_{\\mathrm{br}} = w_O$ (Eq. 5), in which case the input-port occupations of the branched optimum spell a satisfying assignment, while a strict deficit certifies unsatisfiability. The same compiled graph evaluates the circuit forward when input ports are pinned instead, and mixed pinning answers general constraint queries. The authors verify the equivalence exactly through exhaustive enumeration on the 30-atom three-gate circuit, the 85-atom full adder, and the 165-atom two-bit multiplier, and they report that a closed-system tensor-network simulation of a 4$\\mu$s annealing protocol reaches the MWIS manifold in 58.0% of projective samples on the three-gate instance.","pith_inferences":["An extension the authors leave implicit: the same exhaustive gadget search could be run for NAND, NOR, XNOR, or multi-input gates, potentially shrinking circuits that currently require several composed library gates and reducing routing overhead further.","The near-linear atom scaling for structured feed-forward circuits suggests that circuits with dozens of gates could be compiled onto near-term arrays; whether annealing dynamics still concentrate on the MWIS manifold at that size is an open empirical question the paper does not resolve.","Because the branching criterion is exact only for certified optima, a practical hardware protocol would collect many shots and compare the full weight histogram against $W^{\\star}$ and $W_{\\mathrm{br}}$, turning the equality test into a statistical check rather than a single-sample certificate."],"forward_implications":["Circuit-SAT instances of a few gates fit comfortably on current Rydberg arrays: the three-gate circuit, full adder, and two-bit multiplier compile to 30, 85, and 165 atoms, versus 1257, 2563, and 5060 atoms through the CNF chain.","A single compiled layout can be reused for several tasks at runtime: pinning the inputs evaluates the circuit, pinning the output inverts it and extracts a witness, and pinning a mixed subset of ports poses general constraint queries, all without re-layout.","The output-branching test gives an exact UNSAT certificate only when $W_{\\mathrm{br}}$ is a proven optimum; with analog hardware samples, persistent failure to reach the satisfiable reference weight is the operational signature of unsatisfiability.","For typical structured feed-forward circuits the atom cost grows nearly linearly with gate count, while the worst case remains quadratic with a much smaller constant than the CNF baseline.","A 4$\\mu$s annealing pulse on the compiled three-gate instance reaches the exact ground-state manifold in 58.0% of 1000 projective samples, and 54.6% on the branched certificate graph, indicating the encoded optima are dynamically accessible under a hardware-compatible schedule."],"supporting_citations":[{"why":"Supplies the automated gadget-search method used to find and certify each gate and routing gadget.","marker":"[28]"},{"why":"Provides the weighted wire-chain and arbitrary-connectivity construction that the compiler's wire and routing rules build on.","marker":"[2]"},{"why":"Defines the CNF transformation that serves as the baseline the direct encoding is measured against.","marker":"[25]"},{"why":"Demonstrates weighted MWIS on Rydberg arrays via local light shifts, grounding the weight-to-detuning mapping.","marker":"[3]"},{"why":"Establishes the Rydberg MIS correspondence in the blockade limit, the physical basis of the encoding.","marker":"[6]"},{"why":"Introduces Rydberg quantum wires used to embed nonlocal edges in the CNF baseline and informs chain routing.","marker":"[1]"},{"why":"Proves Circuit-SAT NP-complete, fixing the problem's standing and motivating the reduction.","marker":"[22]"},{"why":"Provides the classical branching recurrence for maximum independent set that underlies the branching primitive.","marker":"[33]"}],"fun_headline_variants":["Rydberg gadget compiler cuts Circuit-SAT atom cost 22-fold","Direct MWIS encoding skips CNF, 22x fewer Rydberg atoms","Circuit-SAT solved on Rydberg arrays with 22x fewer atoms","Gate-level compiler: Circuit-SAT to Rydberg MWIS, 22x saving"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The hardware must operate in the hard-blockade limit, where atoms within a fixed radius interact strongly and all farther pairs do not interact at all; any residual interaction beyond that radius, or any deviation in the local detunings, breaks the exact equality between the array's ground state and the compiled graph's maximum-weight independent set.","fun_headline_variants_meta":{"raw":{"variants":["Rydberg gadget compiler cuts Circuit-SAT atom cost 22-fold","Direct MWIS encoding skips CNF, 22x fewer Rydberg atoms","Circuit-SAT solved on Rydberg arrays with 22x fewer atoms","Gate-level compiler: Circuit-SAT to Rydberg MWIS, 22x saving"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000794,"raw_usage":{"total_tokens":3573,"prompt_tokens":1101,"completion_tokens":2472,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":717,"completion_tokens_details":{"reasoning_tokens":2385}},"tokens_in":717,"tokens_out":2472,"duration_ms":18456,"temperature":1.0,"reasoning_tokens":2385,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T20:13:51.400871+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Compile a known satisfiable and a known unsatisfiable circuit, branch the output port, and run exact classical MWIS on both the full and branched graphs: if any maximum-weight independent set of the full graph projects to a row outside the circuit truth table, or if satisfiable instances fail to satisfy $W^{\\star} - W_{\\mathrm{br}} = w_O$ while unsatisfiable instances satisfy it, Theorem 1 falls. A hardware test would measure the final-state weight distribution after the 4$\\mu$s pulse on the 30-atom layout and check whether the most probable weight is $W^{\\star}=23$ for the full graph and $W_{\\mathrm{br}}=22$ for the branched graph; a systematic shortfall would indicate residual interactions or detuning errors beyond the hard-blockade model.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines the CNF transformation that serves as the baseline the direct encoding is measured against."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Demonstrates weighted MWIS on Rydberg arrays via local light shifts, grounding the weight-to-detuning mapping."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Introduces Rydberg quantum wires used to embed nonlocal edges in the CNF baseline and informs chain routing."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Proves Circuit-SAT NP-complete, fixing the problem's standing and motivating the reduction."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the classical branching recurrence for maximum independent set that underlies the branching primitive."}],"review_version":1}