{"id":"4ab91aee-83bc-4c6c-98d1-787ed51dd682","arxiv_id":"2506.23784","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"A GNN that ranks conjunctive word equations improves the solved-problem count of a Nielsen-transformation solver on synthetic linear benchmarks.","lead":"Word equations are string constraints used in program verification; this paper trains a graph neural network to decide which equation the solver should process first. On synthetic benchmarks where each variable appears at most once per equation, the learned ranking lets their solver finish more problems than established SMT string solvers.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The headline result may be an artifact of test-set selection: Table 4 chooses the best of 15 task/option configurations on the same 1000-problem evaluation used in Table 2, and the margins over Z3 are only 8 (A1) and 17 (A2) solved problems, with no error bars.","rationale":"The reader's weakest-assumption centers on the training-label heuristic (shortest MUS conjunct, shortest UNSAT path) possibly mismatching the real objective. That is a reasonable concern for the internal learning story, but it is not the most load-bearing threat to the central claim: even a poorly motivated label could accidentally produce a better solver, and the paper's negative result on Benchmark C is outside the claimed linear-benchmark setting. The more direct threat is the validity of the reported comparison itself. Table 4 reports solved counts for 15 configurations on the evaluation set, and the rows labeled GNN-DragonLi in Table 2 are the bold best entries (Task 2, RE5) selected on that same set. Because the margins over Z3 are small (8 problems on A1, 17 on A2), and because some configurations fall below Z3 (e.g., Task 3/RE5 on A2 gives 875 vs Z3's 878), the central claim is not robust unless a configuration is fixed before evaluation and variance across benchmark samples is reported. The stochastic baseline RE2 is also a single run, so the claimed advantage over random ordering is not quantified. These issues are empirically checkable; if a pre-registered configuration on fresh samples preserves the advantage, the claim stands. Thus the conditional verdict remains appropriate, but the condition should be the evaluation protocol rather than the labeling assumption.","tokens_in":20476,"tokens_out":9805,"duration_ms":104587,"concrete_test":"Pre-register one configuration before seeing the test set (e.g., Task 2 with RE5, chosen on validation). Generate 10 independent 1000-problem samples from the A1 and A2 generators; run GNN-DragonLi, DragonLi, and the best SMT solver (Z3/cvc5) with the same 300s timeout. Report per-sample solved counts and the mean difference with 95% CI. Additionally, run Random-DragonLi with 10 seeds on the original test set. If GNN-DragonLi's mean solved count does not exceed Z3/cvc5 by more than the CI in a majority of samples, the central claim is not supported.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 6.1's Table 2 reports GNN-DragonLi from the bold entries of Table 4, which evaluates Tasks 1-3 x RE3-RE7 (15 configurations) on the same 1000-problem benchmark and selects the best per benchmark (Task 2, RE5). Selecting the maximum over 15 configurations on the test set inflates the reported solved count. The fragility is visible in Table 4: on A1, Task 1/RE5 solves 978 problems, barely above Z3's 977, while Task 2/RE5 solves 985; on A2, Task 3/RE5 solves 875, below Z3's 878, whereas Task 2/RE5 solves 895. Thus whether the central claim holds depends on which of the 15 configurations is chosen. In addition, RE2/Random-DragonLi is a single random ordering with no standard error, so the 45-problem gap between GNN-DragonLi and Random-DragonLi on A2 is not necessarily significant. The training-label assumption (Eqs. 3-4) is a secondary concern: the empirical comparison could hold even if labels are imperfect.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper extends a Nielsen-transformation-based word equation solver (DragonLi) by adding a ranking module that reorders conjuncts before each inference-rule application. It proposes a graph encoding of a conjunctive word equation enriched with global term-occurrence information, three multi-classification formulations that produce per-conjunct scores, and seven RankEqs options combining the trained GNN with the existing heuristic. Training labels are derived from MUSes computed by external solvers and from shortest UNSAT paths in the solver's AND-OR trees. Experiments on four synthetic benchmarks compare the resulting GNN-DragonLi against Z3, cvc5, Z3-Noodler, Ostrich, and Woorpje; the headline claim is that on the two linear benchmarks A1 and A2, GNN-DragonLi solves 985/1000 and 895/1000 problems, respectively, more than any of the other solvers.","tokens_in":20796,"tokens_out":6349,"duration_ms":68969,"significance":"If the results hold, the paper makes a useful contribution to learning-guided word equation solving: the ranking problem for conjunctive word equations is natural and unexplored, the graph representation with global occurrence counts is a reasonable way to give the GNN a system-level view, and the authors provide a fairly complete experimental package including benchmarks, a repository, hyperparameters, and ablations over tasks and ranking options. The soundness of the extended algorithm follows directly from the existing calculus and is stated as Lemma 1. However, the headline improvement over Z3 is only 8 solved problems on A1 and 17 on A2 out of 1000, and the paper's own ablation shows that the reported configuration is selected as the best among 15 task/RE combinations evaluated on the same test set. The central claim is therefore less robust than the abstract suggests and needs additional validation before it can be accepted as stated.","major_comments":[{"comment":"The reported GNN-DragonLi result is the configuration with the best UNSAT count among 3 training tasks × 5 RE options (15 configurations), all evaluated on the same 1000-problem test set used for the comparison with other solvers. The selection issue is concrete: on A1, Task 1/RE5 solves 978 problems, only one more than Z3's 977, and Task 3/RE5 solves 975; on A2, Task 3/RE5 solves 875, below Z3's 878, while Task 2/RE5 solves 895. Thus whether the abstract's claim holds depends on which of the 15 configurations is chosen, and the paper gives no validation-based or otherwise pre-registered selection rule. To support the central claim, model/task/RE selection must be performed on a held-out validation set or through a nested procedure, and the test-set counts for all configurations should be presented with the selection rule stated explicitly.","section":"§6.1 / Appendix B.5, Table 4"},{"comment":"RE2 and RE4 are stochastic ranking heuristics, but the paper reports only a single run for each: RE2 appears as one random ordering and RE4 as one run of a 50%-random mechanism, with no seeds, repetitions, or confidence intervals. Since the GNN-DragonLi versus Random-DragonLi gap is 19 solved problems on A1 and 45 on A2, and Table 4 shows that the random component in RE4 can change UNSAT counts by hundreds of problems across benchmarks and tasks (e.g., A2 Task 2 RE3 versus RE4: 300 vs. 468 UNSAT), the claimed superiority of learned ranking over random ranking is not statistically supported. The authors should report multiple seeds for all stochastic options and, if possible, the resulting variance.","section":"§4.4 and §6.1, Table 2"},{"comment":"The labeling rules encode two unvalidated optimality assumptions: that the shortest equation in a MUS is the best conjunct to process first, and that the shortest UNSAT path in the AND-OR tree is the optimal ranking target. The only supporting evidence is Table 1's 'DragonLi using MUS' row, which shows the heuristic succeeds on only 57–58% of MUS-bearing problems on A1/A2, 20% on B, and 0% on C, and no comparison is made against models trained with alternative labels (e.g., all MUS conjuncts, or labels derived from actual solving time or split counts). Because the GNN's training signal is exactly this proxy, an ablation comparing labeling schemes is needed to show that the chosen rule, rather than any MUS-derived signal, is responsible for the improved solving counts.","section":"§4.1, Eqs. (3)–(4)"}],"minor_comments":[{"comment":"The text has a typo in 'it is know to be NP-hard' (should be 'known'), and the Preliminaries heading 'W ord Equations' has an extra space.","section":"§1 and §2"},{"comment":"The solver is spelled 'Woopje' in the main text but 'Woorpje' in Table 2 and reference [16]; please unify the spelling.","section":"§6.1 and Table 2"},{"comment":"The caption should define the subcolumns CS and CU and explain that split counts are averages over commonly solved problems only; as presented, the table is difficult to parse.","section":"Table 2"},{"comment":"The padding of formulas with fewer than n equations by 'empty equations' is not defined for the graph encoding; please clarify how an empty equation is represented and whether padded positions are masked in the loss.","section":"§4.3, Task 3"},{"comment":"Adding a 'total solved' column would let the reader verify the headline counts without manually summing the SAT and UNSAT columns.","section":"Table 4"}],"recommendation":"major_revision","confidential_remarks":"I lean major revision rather than reject because the underlying idea and experimental infrastructure are sound and the flaws are fixable. The authors should be asked to (1) perform model/task/RE selection on a validation set or otherwise justify the chosen configuration without using test-set performance, (2) report multiple seeds for stochastic baselines and the GNN training itself, and (3) include an ablation of the labeling assumptions. If the ranking advantage survives those checks, the paper would be a solid contribution."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: competent engineering, real but modest result, with a model-selection issue that needs fixing before the headline claim is fully persuasive.\n\nWhat's new: this is the first application of GNN-based ranking (not branching) to word equation solving. The graph encoding that carries global occurrence counts across conjuncts is a clean idea, and the three task formulations are a reasonable way to adapt multi-classification to variable-length ranking. The experimental section is honest and thorough: ablations over tasks and integration options, comparisons with five strong solvers, and a clear statement that the heuristic collapses on highly non-linear benchmarks. Training on MUSes from external solvers plus shortest UNSAT paths is supervised learning, not circular reasoning.\n\nMain soft spot: the headline numbers come from Table 4's best configuration per benchmark. That's 15 task/option combinations evaluated on the same 1000-problem test set, and the paper doesn't say the choice was made on validation rather than test. The fragility is real: on A1, Task 1/RE5 gives 978 solved, essentially tied with Z3's 977; on A2, Task 3/RE5 gives 875, worse than Z3's 878. So the claimed edge of 8 and 17 problems is well within configuration noise. This doesn't sink the paper, but it does mean the central claim is weaker than the abstract suggests.\n\nSecondary issues: the random baseline is a single run with no seeds or confidence intervals, so the 45-problem gap over random on A2 could be part noise. The labeling assumptions (shortest MUS conjunct is the best next equation; shortest UNSAT path is the optimal ranking) are plausible but unvalidated against the actual objective. Those are minor, and an imperfect label could still yield a working ranking.\n\nWho this is for: anyone building learning-based heuristics for string or word equation solvers. The result is limited to synthetic linear benchmarks, and the paper is transparent about that. If the configuration-selection question is answered with validation-based selection and the stochastic baselines get error bars, this becomes a solid contribution. Worth sending to review with that request attached.","headline":"Competent engineering with a real but modest result; the main claim needs validation-based model selection and error bars before it fully holds up.","tokens_in":21252,"tokens_out":4028,"would_cite":true,"duration_ms":39931,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"A graph neural network that ranks word equations before each splitting step enables a Nielsen-transformation solver to solve more linear word-equation problems than five state-of-the-art string solvers.","keywords":["word equations","graph neural networks","learning to rank","minimal unsatisfiable subsets","string solving","Nielsen transformation","SMT solvers","conjunctive word equations"],"falsifier":"Compute the correlation between the training label (shortest conjunct in an MUS) and the conjunct that actually lies on the shortest UNSAT path in the solver's AND-OR tree across the 909 Benchmark A1 problems with extractable MUSes; if the correlation is near zero, the GNN's gains cannot be attributed to the MUS-derived signal. A second check is to run GNN-DragonLi on a fresh linear benchmark where the shortest MUS conjunct is deliberately not the fastest to prove UNSAT: if solved problems and split counts do not improve over the fixed heuristic, the ranking proxy is the wrong mechanism.","tokens_in":20299,"feed_emoji":"🧩","tokens_out":8791,"duration_ms":88202,"temperature":0.7,"pith_summary":"The paper tries to establish that the order in which a word-equation solver processes the conjuncts of a formula can be learned, and that a graph neural network trained on unsat-core information makes a Nielsen-transformation solver solve more linear word-equation problems than established string solvers. The motivation is that in this calculus each ranking decision decides where the AND-OR search tree grows; a bad choice can send the solver down infinite branches, while a good choice reveals unsatisfiability quickly. On two linear benchmarks, where each variable appears at most once in each equation, the GNN-ranked variant solves 985 and 895 of 1,000 problems, ahead of cvc5, Z3, Z3-Noodler, Ostrich, and Woorpje. The authors also report that on non-linear benchmarks the advantage shrinks (Benchmark B) and disappears entirely (Benchmark C), which they attribute to the calculus rather than the ranking. The broader claim is that learned ranking of symbolic subgoals is a transferable recipe for improving decision procedures.","feed_headline":"GNN ranking solves 985 of 1,000 linear word problems","feed_subtitle":"Learned conjunct ordering beats five established solvers on linear word-equation benchmarks.","key_machinery":"The central mechanism is the RankEqs step inserted into the split algorithm, which reorders the conjuncts so that the leftmost equation is the one the inference rules rewrite next. To make this decision learnable, each equation is encoded as a graph whose syntax-tree nodes are augmented with binary-encoded global occurrence counts of every variable and letter across the whole conjunction, so the GCN can see each equation in context. Three adaptations of a multi-classification model turn per-equation embeddings into a ranking: a per-equation softmax, a softmax conditioned on the aggregated global embedding, and a fixed-window classifier with padding and trimming. The model is trained with categorical cross-entropy against labels that mark either the shortest equation in a minimal unsatisfiable subset or the equation on the shortest path to UNSAT in the AND-OR tree, with the constraint that exactly one conjunct is labeled 1 per training point.","core_discovery":"The paper's central claim is that ranking conjuncts before each application of the inference rules is a learnable and performance-critical step, and that GNN-based ranking trained on minimal unsatisfiable subsets (MUSes) and on shortest paths to UNSAT in the solver's AND-OR tree outperforms fixed and random ranking heuristics on linear benchmarks. In the main comparison, GNN-DragonLi solves 985 of 1,000 problems on Benchmark A1 and 895 of 1,000 on Benchmark A2, more than cvc5, Z3, Z3-Noodler, Ostrich, and Woorpje, while also reducing the average number of splits on commonly solved problems. The authors present this as evidence that the ranking process—not just the underlying calculus—determines solver efficiency, and that the training signal from unsat cores transfers to better decisions on unseen problems.","pith_inferences":["The labels used for training are proxies, and the paper's results leave implicit that the shortest conjunct in an MUS must also be the conjunct whose early processing closes the proof fastest; a benchmark where these two notions disagree would test whether the GNN learned the intended behavior or just a shortcut.","The same ranking machinery should transfer to other symbolic procedures that must choose among formulas or constraints—for instance ordering assertions inside an SMT solver or selecting clauses in a saturation-based prover—because the graph encoding and ranking heads are not word-equation-specific.","The ablation pattern in which one-shot GNN invocation (RE5) usually matches or beats calling the model at every step suggests the practical recipe is to let the GNN fix an early ordering and let the deterministic calculus take over, minimizing model-call overhead.","Benchmark C's zero-label collapse indicates that a natural next step is to combine learned ranking with length- or letter-count-based filters for non-linear equations, and that without such filters the method's scope is confined to mostly linear input systems."],"forward_implications":["On the two linear benchmarks, the GNN-ranked solver solves more problems than the fixed heuristic, the randomized reordering, and all five external solvers, so the learned ordering is the source of the extra solved instances.","Because the training signal comes from MUSes computed by existing solvers and from shortest UNSAT paths, existing solver runs can be recycled into ranking supervision without hand-designed features.","The three multi-classification adaptations allow the same fixed-size GNN to rank conjunctions of any size, so the approach applies to systems with 1 to 100 conjuncts.","On non-linear benchmarks the ranking benefit shrinks (Benchmark B) and vanishes (Benchmark C), which the authors attribute to the calculus generating mostly infinite branches when variables repeat; learned ranking alone does not fix non-linearity.","If reimplemented in a compiled language, the algorithm is claimed to run over 100x faster, so the Python-based solving times reported here understate the practical headroom of GNN-guided ranking."],"supporting_citations":[{"why":"Supplies the Nielsen-transformation calculus, the split algorithm that the ranking step extends, and the base graph encoding.","marker":"[7]"},{"why":"Provides the benchmark-generation approach and the SAT-based word equation solver Woorpje used as a baseline.","marker":"[16]"},{"why":"Z3 is both a comparison baseline in Table 2 and one of the solvers whose MUSes provide training labels.","marker":"[31]"},{"why":"cvc5 is both a comparison baseline and a source of MUS-based training data.","marker":"[10]"},{"why":"Z3-Noodler is an automata-based string solver used as a baseline and as a source of MUSes for training.","marker":"[15]"},{"why":"Ostrich is a string solver used as a baseline and as a source of MUSes for training data.","marker":"[14]"}],"fun_headline_variants":["GNN ranking beats five solvers on linear word equations","Ranking equations with GNNs outperforms cvc5, Z3 on linear benchmarks","Graph neural networks rank word equations to solve more problems","Learning to rank conjuncts improves word equation solving","GNNs learn equation order to beat established string solvers"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the shortest equation in a minimal unsatisfiable subset is the best equation for the solver to attack first, and that shortest paths to UNSAT in the search tree are the right ranking targets; if these proxies disagree with what actually minimizes timeouts or splits, the GNN learns a misleading ranking.","fun_headline_variants_meta":{"raw":{"variants":["GNN ranking beats five solvers on linear word equations","Ranking equations with GNNs outperforms cvc5, Z3 on linear benchmarks","Graph neural networks rank word equations to solve more problems","Learning to rank conjuncts improves word equation solving","GNNs learn equation order to beat established string solvers"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.0002,"raw_usage":{"total_tokens":1355,"prompt_tokens":903,"completion_tokens":452,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":519,"completion_tokens_details":{"reasoning_tokens":366}},"tokens_in":519,"tokens_out":452,"duration_ms":4828,"temperature":1.0,"reasoning_tokens":366,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T21:32:03.487699+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Compute the correlation between the training label (shortest conjunct in an MUS) and the conjunct that actually lies on the shortest UNSAT path in the solver's AND-OR tree across the 909 Benchmark A1 problems with extractable MUSes; if the correlation is near zero, the GNN's gains cannot be attributed to the MUS-derived signal. A second check is to run GNN-DragonLi on a fresh linear benchmark where the shortest MUS conjunct is deliberately not the fastest to prove UNSAT: if solved problems and split counts do not improve over the fixed heuristic, the ranking proxy is the wrong mechanism.","supporting_citations":[{"cited_title":"In: Akshay, S., Niemetz, A., Sankara- narayanan, S","cited_arxiv_id":null,"evidence_quote":"Supplies the Nielsen-transformation calculus, the split algorithm that the ranking step extends, and the base graph encoding."},{"cited_title":"In: Filiot, E., Jungers, R., Potapov, I","cited_arxiv_id":null,"evidence_quote":"Provides the benchmark-generation approach and the SAT-based word equation solver Woorpje used as a baseline."},{"cited_title":"In: 2008 Tools and Algo- rithms for Construction and Analysis of Systems","cited_arxiv_id":null,"evidence_quote":"Z3 is both a comparison baseline in Table 2 and one of the solvers whose MUSes provide training labels."},{"cited_title":"In: Fisman, D., Rosu, G","cited_arxiv_id":null,"evidence_quote":"cvc5 is both a comparison baseline and a source of MUS-based training data."},{"cited_title":"In: Finkbeiner, B., Kov´ acs, L","cited_arxiv_id":null,"evidence_quote":"Z3-Noodler is an automata-based string solver used as a baseline and as a source of MUSes for training."}],"review_version":1}