Pith. sign in

REVIEW 5 minor 1 cited by

Provably Good Prim-Dijkstra Revisited: New Theory and a Practical Algorithm for a Classical VLSI Routing Problem with LLMs

T0 review · 0 major / 5 minor · reviewed 2026-08-01 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper settles a 1992 open problem in VLSI routing: the terminal-only Manhattan cost–radius spanning-tree problem is NP-complete, and a simple height partition of a rooted MST yields a tree whose total length and root-to-terminal radius

desk verdict A careful, honestly-scoped paper that settles a real open complexity question and gives a clean (2,2) tradeoff; the terminal-only boundary is the main caveat, but the paper never overclaims. read the letter →

arxiv 2607.17005 v1 pith:DMR6H7AV submitted 2026-07-18 cs.AR cs.DS

Keren Zhu This is my paper · ORCID
classification cs.ARcs.DS MSC 68Q1768R1005C0568W25
keywords Prim-Dijkstraroutingcost-radiusspanningtreebicriteriaapproximationweakNP-completenessManhattanmetricheightpartitionVLSIperformance-driven
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper revisits Prim–Dijkstra routing: given terminals in the Manhattan plane, a single root, and a complete graph of possible edges, find a spanning tree with bounded total wirelength L and bounded root-to-sink path length R. The author proves that the natural decision version—does a tree exist with L ≤ B and R ≤ D?—is NP-complete, via a weak reduction from integer Partition, answering a question left open since 1992. On the positive side, the paper gives a bottom-up height partition of a rooted MST that returns, for any threshold H, a tree with R ≤ Δ + H and (L − M)H ≤ MΔ, where M is the MST length and Δ the maximum root distance; choosing H = Δ yields the balanced guarantee L ≤ 2M and R ≤ 2Δ. The paper packages this into HP-RCRST, a deterministic solver whose certified mode always contains such a (2,2) tree and whose empirical modes, on the paper's benchmark set, Pareto-dominate the union of published methods on 23 of 28 instances and tie on the other five. A sympathetic reader should care because the work closes a long-standing complexity question, supplies an unusually simple certified approximation for a practical routing objective, and illustrates a reusable workflow for reopening dormant algorithmic problems.

What carries the argument

The load-bearing object is the rooted complete-terminal Manhattan graph with the two objectives L(T)=sum of edge lengths and R(T)=max root-to-terminal path length, normalized against the MST length M and the maximum root distance Δ. For hardness, the machinery is an explicit Partition gadget whose coordinate and budget choices force a feasible tree to correspond exactly to a subset of sum S/2; the proof uses interblock prefix-cut forcing and a bridge inequality to eliminate all noncanonical complete-graph edges. For approximation, the machinery is Algorithm 1 (HeightPartition): in postorder, keep a parent edge if the residual height stays within H, otherwise replace it with a direct root edg

What would settle it

Run HeightPartition on any finite metric instance and independently remeasure the output: the theorem predicts R ≤ Δ+H and (L−M)H ≤ MΔ, so a single violation falsifies Theorem 4.2; for the complexity claim, a pseudopolynomial exact algorithm for the terminal-only Manhattan decision problem would contradict the weak NP-hardness result.

Watch

Extended reading notes

Core claim

The central discovery is that the terminal-only Manhattan version of the bounded-cost bounded-radius spanning-tree problem is computationally hard in the weak sense, yet admits a linear-time, MST-based construction with a balanced bicriteria guarantee. The reduction from Partition is explicit and numerical: terminals are placed at integer coordinates so that any feasible tree encodes a subset summing to S/2, and a cut-forcing argument rules out every other complete-graph edge. The approximation result is the height partition: process a rooted MST bottom-up, cutting a parent edge whenever the accumulated subtree height would exceed H, and reconnecting that subtree root directly to the source.

Load-bearing premise

All theorems assume terminal-only spanning trees—no Steiner points—with a single root and the same Manhattan metric used for both total cost and path length; if the intended VLSI application allows Steiner vertices, the NP-completeness result and the (2,2) construction do not transfer as stated.

Editorial extensions

If this is right

  • The decision problem is weakly NP-complete: no polynomial-time exact algorithm exists for the rooted, terminal-only Manhattan cost-radius problem unless P=NP, closing the 1992 question.
  • For every H>0, HeightPartition returns a tree with normalized guarantee (L/M, R/Δ) ⪯ (1+Δ/H, 1+H/Δ); the balanced choice H=Δ gives a single tree with L≤2M and R≤2Δ.
  • The construction runs in linear time after the MST is rooted, so a fast deterministic router can carry a certified (2,2) guarantee; HP-RCRST's certified mode always emits such a tree or an exact Pareto dominator.
  • In arbitrary metric spaces, no single tree can be certified with common factor below two by these arguments (trunk-and-arms lower bound); beating two requires planar L1 structure or a portfolio of trees, both left open.
  • On the paper's 28 development instances, the stronger empirical modes of HP-RCRST Pareto-dominate the union of published methods on 23 cases and tie on the remaining five; its certified mode does not dominate that union but offers the theorem-backed witness.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Inference: Because the hardness reduction is weak and numerical, a pseudopolynomial exact algorithm for the terminal-only Manhattan problem is a plausible research target; the explicit coordinate construction shows exactly where bit sizes matter.
  • Inference: The height-partition charging scheme—charging each shortcut to the residual component that violated the threshold—is a transferable amortization template for other bicriteria spanning-tree problems in metric spaces.
  • Inference: The paper's empirical split between a good central compromise and weak frontier shoulders suggests a design principle beyond this instance: a certified one-parameter family is a reliable backbone, but articulating a full tradeoff curve requires search that can change MST topology.
  • Inference: The observation that many MSTs share the same length but different root radii points to a concrete improvement: searching over MST tie structures, rather than thresholds on one canonical MST, may close much of the remaining gap between certified and empirical modes.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

0 major / 5 minor

Summary. The paper revisits the rooted, terminal-only Manhattan cost–radius spanning-tree problem: find a spanning tree of a complete terminal graph, with Manhattan edge lengths, satisfying total cost bound B and root-to-terminal radius bound D. It claims three main theoretical results: (1) weak NP-completeness of the decision problem via a polynomial-time reduction from Partition (Theorem 4.1, Appendix A); (2) a continuous cost–radius tradeoff for a bottom-up height partition of a rooted MST, giving rho(A_H) <= (1+Delta/H, 1+H/Delta) and in particular a (2,2) guarantee at H=Delta (Theorem 4.2, Appendix B); (3) an arbitrary-metric lower bound showing that no single tree can have a universal common factor below 2 (Theorem B.4). The paper then presents HP-RCRST, a deterministic solver with one certified mode carrying the (2,2) guarantee and three empirical modes, and evaluates it on 28 development instances, 50 held-out instances, and scaling runs to n=2048. The paper is explicit that the model is terminal-only, that NP-hardness is weak, that the main theorems are not Lean-formalized, and that the empirical frontier claims are scoped to the development set.

Significance. If the results hold, they settle a complexity question left open in 1992 in the weak sense, give an unusually simple certified (2,2) construction, and provide a reproducible solver with careful exact remeasurement. The strengths are real: the NP-completeness reduction is self-contained and includes the cut-forcing lemmas, the bridge inequality, and bit-complexity accounting; the height-partition proof rests on a valid disjoint-charge argument over MST edges; the arbitrary-metric lower bound is internally consistent; and the empirical claims are explicitly limited and backed by exact integer validation. The paper also transparently states which parts are not formalized or not released. I found no load-bearing flaw in the central derivations.

minor comments (5)
  1. [Appendix A.3, Eq. (13)] The displayed equation L = X + 2A + 4(S-A) = X + 3S is algebraically false for general A; it becomes X + 4S - 2A, which equals X + 3S only after substituting A = S/2. The main text in Section 4.1 gives the correct form L = X + 4S - 2A = B. Please correct or rephrase the appendix line to avoid confusion in a proof appendix.
  2. [Appendix A.4, bridge inequality] The telescoping expression H_b = X - 3A+ + 3A- assumes every bridge is traversed left-to-right on P. This follows from Lemma A.1's c_P = 1 on each interblock cut, but the appendix does not state it explicitly. Add a sentence making this justification clear.
  3. [Sections 5.4, Alg. 3, C.4] The mode name is written both as 'qality' and 'quality'. Standardize the spelling, since the inconsistency is distracting in pseudocode and policy tables.
  4. [Section 6.2 / Appendix D] The direct comparisons against PD-II and the terminal MSPD/MSS portfolio are reported in the text but the corresponding per-baseline tables are not shown; the reader must infer them from the raw-data description. A small table or pointer to the exact rows would improve verifiability.
  5. [References] Several references, especially [22], [27], and [30], are to very recent or non-archival sources. Please confirm they are publicly available and stable before final publication, or mark them as preprints.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the theoretical results are self-contained and the empirical claims are explicitly development-scoped, with no load-bearing self-citations.

full rationale

The derivation chain is self-contained rather than circular. Theorem 4.1 gives an explicit many-one reduction from Partition, with a forward construction and an independent reverse argument using cut-forcing Lemmas A.1-A.2 and the bridge inequality Lemma A.3; the NP-hardness conclusion does not presuppose the target problem. Theorem 4.2 proves parameter-free bounds R(A_H) <= Delta + H and (L(A_H)-M)H <= M Delta from MST cut optimality and a residual-height invariant; the H = Delta choice is the symmetric substitution yielding (2,2), not a fitted constant or a renamed input. The empirical section is candid about its scope: 'Because these 28 instances were visible during development, we use them for regression and direct baseline comparison, not as evidence of out-of-sample generalization' (Section 6.1), and Appendix C.6 states that universal guarantees are reserved for certified mode while the other modes make only empirical claims. The appended limitations - terminal-only model, weak NP-hardness, and the absence of completed Lean proofs for the main theorems - are verification and scope boundaries, not circular reductions. There are no load-bearing self-citations: the open question is attributed to Cong et al. 1992 and the baselines are external published methods. No fitted parameter is relabeled as a prediction, and no equation is used as its own conclusion.

Assumptions & free parameters 3 free parameters · 5 assumptions · 0 invented entities

The theorem side is nearly free of fitted parameters: H is a continuum knob and H=Δ is the symmetric point. The empirical side carries substantial hand-tuned schedules derived from the 28 development instances plus baseline sweep definitions; these affect only the practical solver claims. The axioms are standard complexity-theory and metric facts together with the explicit terminal-only scope. No new physical or mathematical entities are postulated.

free parameters (3)
  • Height threshold H = H=Δ for the balanced certificate; five sampled thresholds in certified mode
    H is a free parameter of Algorithm 1, but Theorem 4.2 holds for every real H>0, so the central bound is not fit. The balanced choice H=Δ is determined by the two inequalities, not by data.
  • Empirical mode schedules and size cutoffs = 96/48/32 trials, n≤8 Prüfer enumeration, n≤32 intensive search, n≤128 centered DP, n≤256 cap schedule, 8×2 cap beam, com
    These hand-chosen policies were configured on the 28 development instances. They influence the empirical Pareto-dominance claims but not the theorems.
  • Baseline parameter sweeps = PD-II α1=α2=k/20, k=1..19; MSPD/MSS α=j/10 and (κ,λ)∈{1..4}^2
    The published-method union is defined by these sweeps. If they are unrepresentative of the original methods, the empirical comparison weakens.
assumptions (5)
  • standard math Partition is NP-complete under polynomial-time many-one reductions
    The hardness proof in Appendix A uses binary Partition as the source problem, citing Garey and Johnson.
  • standard math MST cut optimality and triangle inequality hold in the complete Manhattan terminal graph
    Theorem 4.2 and the factor-two lower bound rely on e_v ≤ d(r,v) and on MST optimality; these are standard properties of the finite metric setting.
  • domain assumption Exact binary arithmetic on O(nS)-bit integers is polynomial and sufficient for membership checking
    Membership in NP and the certificate-checking argument in Section A.1 depend on exact arithmetic remaining polynomial in the binary input length.
  • domain assumption Terminal-only, single-source, no Steiner vertices
    Section 2.1 explicitly fixes this boundary. The weak NP-completeness proof, the height partition, and the solver all operate in this restricted model.
  • domain assumption The 28 development instances are a fair basis for the empirical Pareto comparison
    The empirical mode claims are scoped to these instances, and the paper discloses that they were visible during development. The held-out set mitigates but does not remove this assumption.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Provably Good Prim-Dijkstra Revisited: New Theory and a Practical Algorithm for a Classical VLSI Routing Problem with LLMs." pith.science (2026). https://pith.science/paper/DMR6H7AV

@misc{pith2026260717005,
  author       = {Pith},
  title        = {Pith review of: Provably Good Prim-Dijkstra Revisited: New Theory and a Practical Algorithm for a Classical VLSI Routing Problem with LLMs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/DMR6H7AV}},
  note         = {Machine review of arXiv:2607.17005}
}
read the original abstract

Large language models may make precise but dormant algorithmic problems practical to revisit, and may expose new paths toward fundamental ones. We demonstrate this possibility through Prim-Dijkstra routing, a classic VLSI problem whose terminal-only Manhattan complexity remained open despite decades of practical work. We prove weak NP-completeness, derive a continuous cost-radius tradeoff with a balanced (2,2) guarantee, and build HP-RCRST, a height-partition-based multi-mode solver. On 28 development instances, its stronger modes Pareto-dominate the published-method union on 23 and tie on five. The case shows how conflicting conjectures, counterexamples, formal checks, and implementation can reopen neglected questions. Code and reproducibility materials are available at https://github.com/CODA-Team/hp-rcrst.

Figures

Figures reproduced from arXiv: 2607.17005 by the authors.

Figure 1
Figure 1. The Prim–Dijkstra problem between its two textbook endpoints. The same 13 terminals are used in all three panels. [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. The knob lineage on one normalized cost–radius [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Bottom-up height partition and its certified tradeoff. The dotted red edge fails the residual-height test and is replaced [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: Two views of the 28-instance comparison with the published-method union. The stronger practical modes cover the [PITH_FULL_IMAGE:figures/full_fig_p009_4.png]
Figure 5
Figure 5. Figure 5: Single-thread end-to-end median time on the scal [PITH_FULL_IMAGE:figures/full_fig_p009_5.png]
Figure 6
Figure 6. Figure 6: The two canonical block choices in the forward reduction. Blue and muted-red paths are combinatorial terminal [PITH_FULL_IMAGE:figures/full_fig_p014_6.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Rethinking Logic Optimization Operators: Theory-Derived Operator Compression via Agentic Source Analysis

    cs.LO 2026-07 conditional novelty 7.0 of 10

    Certified source-level relations collapse 40 synthesis recipe actions to a 31-action Pareto cover and compile into deterministic gates that speed and improve ABC Orchestrate as TACO.

Reference graph

Works this paper leans on

31 extracted references · 12 canonical work pages · cited by 1 Pith paper

  1. [1]

    Alpert, Wing-Kai Chow, Kwangsoo Han, Andrew B

    Charles J. Alpert, Wing-Kai Chow, Kwangsoo Han, Andrew B. Kahng, Zhuo Li, Derong Liu, and Sriram Venkatesh. 2018. Prim-Dijkstra Revisited: Achieving Superior Timing-driven Routing Trees. InProceedings of the 2018 International Symposium on Physical Design. ACM, 10–17. https://doi.org/10.1145/3177540. 3178239

    work page doi:10.1145/3177540 2018

  2. [2]

    Alpert, T

    Charles J. Alpert, T. C. Hu, Dennis J.-H. Huang, Andrew B. Kahng, and David R. Karger. 1995. Prim-Dijkstra Tradeoffs for Improved Performance-Driven Routing Tree Design.IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems14, 7 (1995), 890–896. https://doi.org/10.1109/43.391737

    work page doi:10.1109/43.391737 1995

  3. [3]

    Carvalho and Amadeu A

    Iago A. Carvalho and Amadeu A. Coco. 2023. On Solving Bi-Objective Con- strained Minimum Spanning Tree Problems.Journal of Global Optimization87, 1 (2023), 301–323. https://doi.org/10.1007/s10898-023-01295-8

    work page doi:10.1007/s10898-023-01295-8 2023

  4. [4]

    Gengjie Chen and Evangeline F. Y. Young. 2020. SALT: Provably Good Routing Topology by a Novel Steiner Shallow-Light Tree Algorithm.IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems39, 6 (2020), 1217–1230. https://doi.org/10.1109/TCAD.2019.2894653

    arXiv 2020

  5. [5]

    Otfried Cheong and Changryeol Lee. 2013. Single-Source Dilation-Bounded Minimum Spanning Trees.International Journal of Computational Geometry & Applications23, 3 (2013), 159–170. https://doi.org/10.1142/S0218195913500052

    work page doi:10.1142/s0218195913500052 2013

  6. [6]

    Kahng, Gabriel Robins, Majid Sarrafzadeh, and C

    Jingsheng Cong, Andrew B. Kahng, Gabriel Robins, Majid Sarrafzadeh, and C. K. Wong. 1992. Provably Good Performance-Driven Global Routing.IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems11, 6 (1992), 739–752. https://doi.org/10.1109/43.137519

    work page doi:10.1109/43.137519 1992

  7. [7]

    Siad Daboul, Stephan Held, Bento Natura, and Daniel Rotter. 2023. Global Interconnect Optimization.ACM Transactions on Design Automation of Electronic Systems28, 5 (2023), 72:1–72:24. https://doi.org/10.1145/3587044

    work page doi:10.1145/3587044 2023

  8. [8]

    Michael Elkin and Shay Solomon. 2015. Steiner Shallow-Light Trees Are Expo- nentially Lighter than Spanning Ones.SIAM J. Comput.44, 4 (2015), 996–1025. https://doi.org/10.1137/13094791X

    doi:10.1137/13094791x 2015

Show all 31 references
  1. [9]

    Josefine Foos, Stephan Held, and Yannik Kyle Dustin Spitzley. 2023. Tighter Approximation for the Uniform Cost-Distance Steiner Tree Problem. InAp- proximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (Leibniz International Proceedings in Infor...

    2023

  2. [10]

    Garey and David S

    Michael R. Garey and David S. Johnson. 1979.Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman

    1979

  3. [11]

    Google DeepMind. 2025. AlphaEvolve: A Gemini-Powered Coding Agent for Designing Advanced Algorithms. https://deepmind.google/blog/alphaevolve-a- gemini-powered-coding-agent-for-designing-advanced-algorithms/

    2025

  4. [12]

    Luis Gouveia, Ana Paias, and Dushyant Sharma. 2008. Modeling and Solving the Rooted Distance-Constrained Minimum Spanning Tree Problem.Computers & Operations Research35, 2 (2008), 600–613. https://doi.org/10.1016/j.cor.2006.03. 022

    2008 doi

  5. [13]

    Stephan Held, Dirk Müller, Daniel Rotter, Rudolf Scheifele, Vera Traub, and Jens Vygen. 2018. Global Routing with Timing Constraints.IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems37, 2 (2018), 406–419. https://doi.org/10.1109/TCAD.2017.2697964

    2018

  6. [14]

    Stephan Held and Edgar Perner. 2025. Cost-Distance Steiner Trees for Timing- Constrained Global Routing. InProceedings of the 62nd ACM/IEEE Design Automa- tion Conference. IEEE, 1–6. https://doi.org/10.1109/DAC63849.2025.11132669

    2025

  7. [15]

    Jan-Ming Ho, D. T. Lee, Chia-Hsiang Chang, and C. K. Wong. 1991. Minimum Diameter Spanning Trees and Related Problems.SIAM J. Comput.20, 5 (1991), 987–997. https://doi.org/10.1137/0220060

    1991 doi

  8. [16]

    Kahng, Shreyas Thumathy, and Mingyu Woo

    Andrew B. Kahng, Shreyas Thumathy, and Mingyu Woo. 2023. An Effective Cost-Skew Tradeoff Heuristic for VLSI Global Routing. In2023 24th International Symposium on Quality Electronic Design. IEEE, 1–8. https://doi.org/10.1109/ ISQED57927.2023.10129350

    2023

  9. [17]

    Ardalan Khazraei and Stephan Held. 2021. An Improved Approximation Algo- rithm for the Uniform Cost-Distance Steiner Tree Problem. InApproximation and Online Algorithms (Lecture Notes in Computer Science), Vol. 12806. Springer, 189–203. https://doi.org/10.1007/978-3-030-80879-2_13

    2021 doi

  10. [18]

    Samir Khuller, Balaji Raghavachari, and Neal E. Young. 1995. Balancing Minimum Spanning Trees and Shortest-Path Trees.Algorithmica14, 4 (1995), 305–321. https://doi.org/10.1007/BF01294129

    1995 doi

  11. [19]

    Tóth, and Tianyi Zhang

    Hung Le, Shay Solomon, Cuong Than, Csaba D. Tóth, and Tianyi Zhang. 2026. Approximating Euclidean Shallow-Light Trees. In42nd International Symposium on Computational Geometry (Leibniz International Proceedings in Informatics), Vol. 367. Schloss Dagstuhl–Leibniz-Zentrum für In...

    2026 doi

  12. [20]

    Adam Meyerson, Kamesh Munagala, and Serge A. Plotkin. 2008. Cost-Distance: Two Metric Network Design.SIAM J. Comput.38, 4 (2008), 1648–1659. https: //doi.org/10.1137/050629665

    2008 doi

  13. [21]

    Jaewon Oh, Iksoo Pyo, and Massoud Pedram. 1997. Constructing Minimal Spanning/Steiner Trees with Bounded Path Length.Integration, the VLSI Journal 22, 1–2 (1997), 137–163. https://doi.org/10.1016/S0167-9260(97)00009-6

    1997 doi

  14. [22]

    OpenAI. 2026. A Proof of the Cycle Double Cover Conjecture. https://cdn.openai. com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_proof.pdf

    2026

  15. [23]

    Bernardino Romera-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M. P. Kumar, Emilien Dupont, Francisco J. R. Ruiz, Jordan S. Ellen- berg, Pengming Wang, Omar Fawzi, Pushmeet Kohli, and Alhussein Fawzi. 2024. Mathematical Discoveries from Program Search with...

    2024 doi

  16. [24]

    Salama, Douglas S

    Hussein F. Salama, Douglas S. Reeves, and Yannis Viniotis. 1997. The Delay- Constrained Minimum Spanning Tree Problem. InProceedings of the Second IEEE Symposium on Computers and Communications. IEEE, 699–703. https: //doi.org/10.1109/ISCC.1997.616089

    1997

  17. [25]

    Dae Young Seo, D. T. Lee, and Tien-Ching Lin. 2009. Geometric Minimum Diameter Minimum Cost Spanning Tree Problem. InAlgorithms and Computation (ISAAC 2009) (Lecture Notes in Computer Science), Vol. 5878. Springer, 283–292. https://doi.org/10.1007/978-3-642-10631-6_30

    2009 doi

  18. [26]

    Shay Solomon. 2015. Euclidean Steiner Shallow-Light Trees.Journal of Compu- tational Geometry6, 2 (2015), 113–139. https://doi.org/10.20382/jocg.v6i2a7

    2015 doi

  19. [27]

    Terence Tao et al. 2026. From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier. arXiv:2607.07779 [cs.AI]

    2026 arXiv

  20. [28]

    Trinh, Yuhuai Wu, Quoc V

    Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, and Thang Luong. 2024. Solving Olympiad Geometry without Human Demonstrations.Nature625, 7995 (2024), 476–482. https://doi.org/10.1038/s41586-023-06747-5

    2024 doi

  21. [29]

    Prenger, and Animashree Anandkumar

    Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J. Prenger, and Animashree Anandkumar. 2023. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. InAdvances in Neural Information Processing Systems, Vol. 36

    2023

  22. [30]

    Cunxi Yu and Haoxing Ren. 2026. Autonomous Evolution of EDA Tools: Multi- Agent Self-Evolved ABC. InProceedings of the 63rd ACM/IEEE Design Automation Conference. https://doi.org/10.1145/3770743.3804221 arXiv:2604.15082 12 Provably Good Prim–Dijkstra Revisited A Complete Weak ...

    2026

  23. [31]

    Construction only

    Consequently the decision problem belongs to NP. A.2 The reduction Given𝑎 1,...,𝑎 𝑛, put 𝑆= ∑︁ 𝑖 𝑎𝑖, ℎ=10𝑆, 𝑡=4𝑆, 𝑋=2ℎ𝑛+𝑡. Create 𝑠𝑖 =(2ℎ𝑖,0) (0≤𝑖≤𝑛), 𝑢 𝑖 =(2ℎ𝑖−3𝑎 𝑖,𝑎𝑖) (1≤𝑖≤𝑛), and𝑧=(𝑋,0), with root𝑠 0. The budgets are 𝐵=𝑋+3𝑆, 𝐷=𝑋+𝑆.(11) Since 𝑥(𝑢𝑖)−𝑥(𝑠 𝑖−1)=2ℎ−3𝑎 𝑖≥17𝑆>0, 𝑥...

Pith tools

Reviewed August 1, 2026 · model on record in the stance chip above.