{"id":"58bc04fd-cbe2-48c5-86cc-5a46e8e2eeef","arxiv_id":"2506.06752","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A SAT-based tool, QuilLS, finds depth-optimal or CX-depth-optimal qubit mappings and runs 10-100x faster than the previous exact tool OLSQ2.","lead":"The authors build a SAT-based layout synthesis tool that provably finds the smallest possible circuit depth, or CX depth, for quantum circuits, and show it runs 10-100x faster than the previous exact tool. This matters because circuit depth and CX count are proxies for how much noise a circuit will suffer on today's quantum hardware.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The SAT encoding's completeness for SWAP-interleaved schedules is asserted but not proven; a brute-force exact comparison on small instances would settle whether the depth-optimality guarantee holds in all cases.","rationale":"The reader's verdict identifies the encoding's missing soundness/completeness proof as the key risk; I agree. I examined the most plausible concrete bug (Eq. 15 forbidding SWAP completions in the first three time steps) and found it is not actually a bug: any SWAP ending at t=3 would occupy layers 1-3 and thus involve only qubits idle throughout those layers, so its effect can be absorbed into the free initial mapping without increasing depth. Thus the constraint does not lose optimality. No other concrete counterexample emerged from reading the constraints. The remaining risk is the unproven general completeness of the SWAP interleaving abstraction. This justifies keeping the CONDITIONAL verdict. A brute-force exact comparison on small instances is the most direct way to settle it.","tokens_in":20788,"tokens_out":42560,"duration_ms":401408,"concrete_test":"Run an exhaustive BFS/DFS exact solver for QLS on all circuits with up to 6 qubits and up to 3 layers on a 2x3 grid and on a 5-qubit path, computing the true minimal depth, and run QuilLS on the same instances. If any instance yields a QuilLS depth greater than the BFS optimum, the encoding is incomplete; if depths match on at least 100 random small instances, the completeness concern is empirically resolved.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is that the SAT encoding of §3, constraints (1)-(20), is exact for depth: satisfiability at makespan t iff a valid mapped circuit of depth t exists, so Algorithm 1's first satisfiable t is the optimum. The paper gives no soundness or completeness theorem for the novel part of the encoding, the three-step SWAP handling (Eqs. 13-19), including interleaving of SWAPs with other gates and ancillary SWAPs. If any valid depth-t circuit is rejected, QuilLS would report overestimates of optimal depth. Empirical agreement with OLSQ2 on shared benchmarks mitigates this risk but does not prove it for all instances, and the absence of a formal argument is especially load-bearing because the tool is advertised as guaranteeing depth-optimality.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents QuilLS, a SAT-based tool for depth-optimal and CX-depth-optimal quantum layout synthesis. The encoding uses incremental SAT solving and parallel plans, with makespan corresponding to circuit depth, and introduces new constraints for scheduling three-step SWAP gates while preserving gate dependencies. The authors claim that the first satisfiable time step in Algorithm 1 yields a mapped circuit of minimal depth or minimal CX-depth, and report speedups of more than 10--100x over the SMT-based OLSQ2 tool on standard benchmarks. The paper also presents an experimental study comparing QuilLS with SABRE, Q-Synth, TB-OLSQ2, and OLSQ2, and an empirical analysis of how different optimization metrics (depth, CX-depth, CX-count) correlate with noise reduction in noisy simulations.","tokens_in":20917,"tokens_out":10609,"duration_ms":108764,"significance":"If the depth-optimality guarantee is formally established, this is a valuable contribution: it is the first SAT-based depth-optimal layout synthesizer, and the reported runtime improvements over OLSQ2 would make exact depth-optimal transpilation practical on substantially larger benchmarks. The paper is strong on the empirical side: it provides a reproducible implementation (GitHub, Zenodo), a broad benchmark suite across multiple platforms, and careful comparisons including locally minimal SWAP counts. The noise correlation study is interesting and appropriately framed as a preliminary empirical finding. The main weakness is that the central optimality claim is asserted rather than proved; a rigorous soundness and completeness argument for the encoding is needed before the 'guarantee' wording in the abstract is justified.","major_comments":[{"comment":"The paper asserts that \"The first time step where the instance is satisfied is the optimal depth\" (Section 3) and that the encoding \"guarantees\" minimal depth (abstract), but no soundness or completeness theorem is provided for constraints (1)--(20). A formal statement is needed: satisfiability of the constraint system at makespan t should be equivalent to existence of a legal mapped circuit of depth t, and the first satisfiable t in Algorithm 1 should be the true optimum. This is load-bearing because the central advertised guarantee depends on it, and the empirical agreement with OLSQ2 on shared benchmarks, while reassuring, does not cover all legal schedules, especially those involving interleaved or ancillary SWAPs.","section":"Section 3, Algorithm 1"},{"comment":"The novel part of the encoding is the handling of three-step SWAPs, but completeness for this part is not argued. In particular, one must show that every legal depth-t mapped circuit, including circuits where SWAPs interleave with other gates on disjoint qubits and where an ancillary (single-occupied) SWAP is used, admits a satisfying assignment of constraints (13)--(19). Conversely, one must show that any satisfying assignment extracts to a valid mapped circuit respecting gate dependencies and connectivity. I recommend adding a proof by construction from an arbitrary feasible mapped circuit to a SAT assignment and the reverse extraction, or at minimum an exhaustive brute-force validation on all small circuits and coupling maps.","section":"Section 3, Eqs. (13)--(19)"},{"comment":"The optimality claim also relies on monotonicity of satisfiability in the makespan t, so that padding a valid depth-t schedule to depth t+1 is always admitted by the constraints, and on monotonicity in the number of SWAPs for the locally minimal SWAP-count search in Section 3.1. Neither monotonicity property is proved; the latter is deferred to a citation [15]. These are elementary but should be stated explicitly, since Algorithm 1's loop otherwise could stop at a non-minimal t if the encoding rejected empty final layers or other padding schedules.","section":"Section 3, Algorithm 1 and Section 3.1"}],"minor_comments":[{"comment":"The pseudocode contains a typo: \"Add M appingConstraints(t)\" should be \"Add MappingConstraints(t)\".","section":"Algorithm 1"},{"comment":"References [22], [23], and [24] all point to the same paper (Tan and Cong, \"Optimality study of existing quantum computing layout synthesis tools\"); these should be consolidated into a single citation.","section":"References"},{"comment":"The spelling of the SAT solver name is inconsistent: \"CaDiCaL\" appears in the tool list and references, while \"CaDiCal\" appears in the text; please unify.","section":"Section 4"},{"comment":"The description of Figure 3 would benefit from stating explicitly what is plotted on each axis; currently the caption only says \"time comparison\" and the axes are not defined in the surrounding text.","section":"Figure 3"},{"comment":"The noise-correlation results report correlation coefficients without confidence intervals or significance tests; given the small set of circuits and a single platform, a brief statement about variability would make the surprising absence of depth--noise correlation easier to interpret.","section":"Section 4.3"},{"comment":"The paper mentions that ancillary SWAPs can be disabled but only presents results with them allowed; a sentence on whether ancillary SWAPs actually occur in the reported solutions would clarify the practical relevance of this option.","section":"Section 3.1"}],"recommendation":"major_revision","confidential_remarks":"The missing soundness/completeness proof is the main obstacle, but it appears fixable within the scope of a revision: the encoding is well-structured and the empirical agreement with OLSQ2 on solved instances is strong evidence that the intended semantics are correct. I would suggest requiring a formal theorem (or, failing that, an exhaustive small-instance verification) as a condition for acceptance, rather than rejecting the paper. The self-citation to Q-Synth [20] is appropriate given the acknowledged lineage, and I see no novelty or attribution concern."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"QuilLS is a real step forward for exact depth-optimal layout synthesis. The empirical speedups over OLSQ2 are credible because the tool ships and the depth values agree with OLSQ2 on shared benchmarks. The main risk is that the encoding's completeness is asserted rather than proved, and the noise study is preliminary.\n\nWhat's new: first SAT encoding where the makespan is circuit depth or CX-depth, with novel handling of three-step SWAPs interleaved with other gates (Eqs. 13-19). The locally-minimal-SWAP extension is a useful practical addition. The experimental section is thorough: 220 benchmark-platform pairs, comparison against SABRE, Q-Synth, TB-OLSQ2, and OLSQ2, with code and data on Zenodo. That is solid, reproducible work.\n\nWhat's good: The speedup claim holds up. QuilLS solves 172-185 instances vs OLSQ2's 95-118, and on solved instances it is often 10-100x faster. The tool agrees with OLSQ2 on optimal depths for shared solved instances, giving real, if partial, evidence that the encoding is exact. The noise correlation finding (CX-count correlates better than CX-depth; combined is best) is genuinely surprising and worth reporting.\n\nSoft spots: The completeness of the encoding is not proved. Constraints (13)-(19) are the novel core, and there is no theorem stating that satisfiability at makespan t iff a legal mapped circuit of depth t exists. If the encoding rejects some valid interleavings (e.g., adjacent three-step SWAPs, ancillary swaps), reported optimal depths could be overestimates. Empirical agreement with OLSQ2 mitigates but does not eliminate this; a brute-force exact check on small random circuits would settle it. That should be added. Also, the noise experiment uses an averaged noise model, one platform, and no error bars on Hellinger distances. The conclusion that depth reduction does not correlate with noise should be tentative, as the authors note.\n\nWho it's for: quantum compilation researchers and anyone using exact layout synthesis. It deserves a serious referee because the tool and data are high quality and the contribution is novel. I recommend engaging, with the main referee asks being: add a soundness/completeness argument or brute-force validation, and either soften the noise claims or add statistical support.","headline":"First SAT encoding for depth-optimal layout synthesis with credible speedups and shipping code; completeness is asserted rather than proved, and the noise study is preliminary.","tokens_in":21462,"tokens_out":2005,"would_cite":true,"duration_ms":18708,"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":"A SAT encoding whose time steps equal circuit depth returns provably minimal-depth quantum layouts, and the paper shows exact depth-optimal transpilation is 10–100x faster than the prior SMT-based tool.","keywords":["quantum layout synthesis","SAT encoding","circuit depth","CX-depth","incremental SAT solving","parallel plans","noise reduction","transpilation"],"falsifier":"Take a small circuit and coupling map (e.g., 4–6 qubits), enumerate all legal mapped circuits of depth at most t by brute force, and check whether QuilLS reports satisfiable exactly when such a circuit exists; any instance where brute force finds a depth-t circuit that the SAT encoding rejects would falsify the claimed optimality guarantee.","tokens_in":20582,"feed_emoji":"⚛️","tokens_out":5671,"duration_ms":52806,"temperature":0.7,"pith_summary":"This paper tries to establish that exact, depth-optimal quantum layout synthesis—rewiring a logical circuit onto a hardware coupling map while preserving gate order—can be solved efficiently with a SAT encoding, implemented in the tool QuilLS. The encoding makes the number of parallel time layers equal the target circuit depth, so the first satisfiable bound is a guarantee of minimal depth or minimal CX-gate depth. On standard benchmarks, QuilLS solves far more instances than the previous exact tool OLSQ2 and is often more than 10–100x faster, though still slower than tools that minimize gate count. The paper also reports a counterintuitive empirical result: reducing CX-count correlates better with noise reduction than reducing depth, and combining CX-count with CX-depth gives the best noise reduction.","feed_headline":"SAT encoding guarantees depth-optimal quantum circuit layouts","feed_subtitle":"Tool QuilLS is 10-100x faster than the prior exact solver, and CX-count beats CX-depth for noise.","key_machinery":"The key machinery is a parallel-plan SAT encoding: each time layer holds independent gates acting on distinct qubits, so the number of layers equals the scheduled circuit's depth. The encoding introduces mapping variables, connectivity predicates, current/advanced/delayed gate flags, and swap variables that span three consecutive layers; a swap variable marks the final step of a SWAP and forces the mappings of the two physical qubits to exchange. An assumption variable enforces that no gate remains delayed at the final layer, and incremental SAT solving reuses learned clauses across increasing depth bounds, so the first satisfiable layer count is certified optimal.","core_discovery":"The central discovery is a propositional encoding of quantum layout synthesis in which the makespan—the number of parallel time layers—directly equals the circuit's depth, with each SWAP gate spread over three consecutive layers and with mapping, connectivity, gate scheduling, and swap effects encoded by the constraint system. By testing satisfiability for increasing makespans starting from the input circuit's depth, the first satisfying assignment is a depth-optimal mapped circuit; preprocessing the circuit to only CX gates gives CX-depth-optimality. The paper claims this is the first SAT-based depth-optimal layout synthesizer, and that on 220 benchmark circuit–platform pairs it is often more than 10–100x faster than the SMT-based depth-optimal OLSQ2 while solving 78% of instances for depth and 84% for CX-depth, versus OLSQ2's 43% and 54%.","pith_inferences":["Inference beyond the paper: if a formal soundness and completeness proof closes the gap the paper leaves open, the same three-layer SWAP encoding could be adapted to other native gate sets, since only the SWAP implementation block would change.","The reported absence of correlation between depth and noise suggests that plain circuit depth may not be a reliable proxy for decoherence; hardware-aware depth metrics that weight idle time could be more predictive. This is my interpretation, not the paper's claim.","A testable extension would add a weighted objective combining CX-count and CX-depth into the SAT makespan, automating the tradeoff the paper identifies as best for noise instead of treating them as separate optimization passes.","The brute-force falsifier described below could be packaged as a small validation suite for future layout-synthesis encodings, checking exact optimality on 4–6 qubit instances."],"forward_implications":["Depth-optimal or CX-depth-optimal transpilation becomes practical for substantially more circuits: on the paper's benchmark set, QuilLS cuts timeouts from OLSQ2's 102–125 down to 35–48.","Because the first satisfiable depth is provably optimal, QuilLS can serve as a ground-truth baseline for evaluating heuristic mappers such as SABRE and near-optimal tools.","The local-SWAP-count variant produces depth-optimal circuits with a minimum number of SWAPs, giving a practical tradeoff point between depth and circuit size.","CX-depth optimization is faster than full depth optimization and, when preceded by a size-optimal pass, gives depths within 1–2% of optimal, making it a cheap default when only CX chains matter.","The empirical correlations suggest that optimizing CX-count together with CX-depth is the better objective for noise reduction, rather than depth alone."],"supporting_citations":[{"why":"Provides the prior SAT encoding for size-optimal layout synthesis whose structure is adapted, and supplies the Q-Synth baseline and benchmark circuits.","marker":"[20]"},{"why":"Introduces OLSQ2, the SMT-based depth-optimal tool that QuilLS is compared against, and supplies benchmark circuits and depth-optimality baselines.","marker":"[15]"},{"why":"Gives SABRE, the heuristic mapper used as a fast baseline and as a provider of upper bounds for the exact tools.","marker":"[13]"},{"why":"Demonstrates incremental and parallel SAT solving for quantum circuit mapping, techniques the paper adapts to the depth-optimal setting.","marker":"[27]"},{"why":"Establishes the parallel-plans technique of encoding plans in propositional logic, which underlies the layer-based makespan representation.","marker":"[10]"},{"why":"Provides the background on conflict-driven clause learning SAT solvers that makes the incremental solving approach effective.","marker":"[16]"},{"why":"Supplies the normalization and correlation-analysis style used in the noise-reduction experiment.","marker":"[26]"}],"fun_headline_variants":["SAT encoding yields depth-optimal quantum layouts","Depth-optimal qubit mapping via SAT, 10-100x faster","Quantum layout: CX-count beats CX-depth for noise","SAT-based layout synthesis guarantees minimum depth","QuilLS: faster depth-optimal quantum circuit mapping"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"That the SAT constraint system is complete: every legal mapped circuit of a given depth satisfies the constraints, so the first satisfiable depth bound is truly the minimum possible depth.","fun_headline_variants_meta":{"raw":{"variants":["SAT encoding yields depth-optimal quantum layouts","Depth-optimal qubit mapping via SAT, 10-100x faster","Quantum layout: CX-count beats CX-depth for noise","SAT-based layout synthesis guarantees minimum depth","QuilLS: faster depth-optimal quantum circuit mapping"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000244,"raw_usage":{"total_tokens":1517,"prompt_tokens":918,"completion_tokens":599,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":534,"completion_tokens_details":{"reasoning_tokens":522}},"tokens_in":534,"tokens_out":599,"duration_ms":6507,"temperature":1.0,"reasoning_tokens":522,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T05:51:00.562331+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a small circuit and coupling map (e.g., 4–6 qubits), enumerate all legal mapped circuits of depth at most t by brute force, and check whether QuilLS reports satisfiable exactly when such a circuit exists; any instance where brute force finds a depth-t circuit that the SAT encoding rejects would falsify the claimed optimality guarantee.","supporting_citations":[{"cited_title":"Kautz, David A","cited_arxiv_id":null,"evidence_quote":"Establishes the parallel-plans technique of encoding plans in propositional logic, which underlies the layer-based makespan representation."},{"cited_title":"Kharkov, Yunong Shi, Marijn J","cited_arxiv_id":null,"evidence_quote":"Supplies the normalization and correlation-analysis style used in the noise-reduction experiment."}],"review_version":1}