Pith. sign in

REVIEW 3 major objections 5 minor 53 references

When GNNs Met a Word Equations Solver: Learning to Rank Equations (Extended Technical Report)

T0 review · 3 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

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

Pith's one-line read 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.

desk verdict Competent engineering with a real but modest result; the main claim needs validation-based model selection and error bars before it fully holds up. read the letter →

arxiv 2506.23784 v1 pith:4FB2BDUK submitted 2025-06-30 cs.AI cs.LG

Parosh Aziz Abdulla , Mohamed Faouzi Atig , Julie Cailler , Chencheng Liang , Philipp Rümmer This is my paper · ORCID
classification cs.AIcs.LG
keywords wordequationsgraphneuralnetworkslearningtorankminimalunsatisfiablesubsetsstringsolvingNielsentransformationSMTsolversconjunctive
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

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

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

  • 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.
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

3 major / 5 minor

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.

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 (3)
  1. [§6.1 / Appendix B.5, Table 4] 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.
  2. [§4.4 and §6.1, Table 2] 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.
  3. [§4.1, Eqs. (3)–(4)] 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.
minor comments (5)
  1. [§1 and §2] 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.
  2. [§6.1 and Table 2] The solver is spelled 'Woopje' in the main text but 'Woorpje' in Table 2 and reference [16]; please unify the spelling.
  3. [Table 2] 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.
  4. [§4.3, Task 3] 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.
  5. [Table 4] Adding a 'total solved' column would let the reader verify the headline counts without manually summing the SAT and UNSAT columns.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the ranking model is trained on externally computed MUSes and evaluated by measured solve counts, with no fitted quantity masquerading as a prediction.

full rationale

The paper makes an empirical claim (GNN-guided ranking solves more linear benchmark problems) and supports it with measured solve counts in Table 2. The training labels (Eq. 3 and Eq. 4 in Section 4.1) are derived from MUSes computed by external solvers (Z3, Z3-Noodler, cvc5, Ostrich) and from traces of DragonLi; neither label is defined in terms of the test-set solved count, so the reported improvement is not forced by construction. The base calculus is taken from the authors' prior work [7], but the inference rules are reproduced in Appendix E and the correctness argument (Lemma 1) is local, so the self-citation is not load-bearing in the ranking claim. The paper's own limitation statements (Section 5.2: Benchmark C yields 0 additional problems solved by the MUS-based heuristic, and consequently no training data or model is generated for Benchmark C) further show that the outcome is not guaranteed by the label heuristic. The selection of the best task/option configuration from Table 4 on the same 1000-problem evaluation is a methodological weakness that could inflate the reported margins over Z3, but it is not circularity: the solved count remains a measured outcome rather than an algebraic consequence of the model's training targets.

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

The empirical claim rests on rules from [7], on the labeling heuristics that define what the network learns, and on the graph encoding; none of these are proved optimal, and validation is only on synthetic benchmarks.

free parameters (3)
  • GNN hyperparameters (hidden size, message-passing rounds) = hidden size 128; rounds per repository
    Hand-chosen architecture constants; no sensitivity analysis is reported, so their effect on the solved-problem counts is unknown.
  • RankEqs integration constants = RE4: 50% random; RE6: n=5000; RE7: n=1000
    Hand-chosen thresholds that control when the GNN is invoked; ablations show different options change solved counts by tens of problems.
  • Training data size = 60,000 problems per benchmark
    Data volume chosen by running the pipeline; Section 6 notes increasing A2 data from 20,000 to 60,000 solves more problems.
assumptions (4)
  • domain assumption Soundness and completeness of the inference rules R1-R9 from [7] (Lemma 1).
    Correctness of Algorithm 1 depends on these rules, which are adopted from the authors' prior paper.
  • ad hoc to paper The shortest equation in a MUS is the most efficient conjunct to process first (Eq. 3).
    This labeling rule is used for all supervised training; its validity is assumed, not proven, and its effectiveness varies from 57-58% on A1/A2 to 0% on C.
  • ad hoc to paper Shortest UNSAT paths in DragonLi's AND-OR trees are good ranking targets (Eq. 4).
    Training source 2 assumes these traces encode optimal ordering; no comparison to other possible optimal orderings is given.
  • domain assumption Binary encoding of global occurrence counts preserves information needed for ranking (Section 4.2).
    This design choice is validated only empirically, and only on the synthetic benchmarks.

how reviews work

0 comments
Cite this review

Pith. "Pith review of When GNNs Met a Word Equations Solver: Learning to Rank Equations (Extended Technical Report)." pith.science (2026). https://pith.science/paper/4FB2BDUK

@misc{pith2026250623784,
  author       = {Pith},
  title        = {Pith review of: When GNNs Met a Word Equations Solver: Learning to Rank Equations (Extended Technical Report)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/4FB2BDUK}},
  note         = {Machine review of arXiv:2506.23784}
}
read the original abstract

Nielsen transformation is a standard approach for solving word equations: by repeatedly splitting equations and applying simplification steps, equations are rewritten until a solution is reached. When solving a conjunction of word equations in this way, the performance of the solver will depend considerably on the order in which equations are processed. In this work, the use of Graph Neural Networks (GNNs) for ranking word equations before and during the solving process is explored. For this, a novel graph-based representation for word equations is presented, preserving global information across conjuncts, enabling the GNN to have a holistic view during ranking. To handle the variable number of conjuncts, three approaches to adapt a multi-classification task to the problem of ranking equations are proposed. The training of the GNN is done with the help of minimum unsatisfiable subsets (MUSes) of word equations. The experimental results show that, compared to state-of-the-art string solvers, the new framework solves more problems in benchmarks where each variable appears at most once in each equation.

Figures

Figures reproduced from arXiv: 2506.23784 by the authors.

Figure 1
Figure 1. AND-OR tree resulting from the word equation [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. The steps for constructing graph representation for the conjunctive word [PITH_FULL_IMAGE:figures/full_fig_p009_2.png] view at source ↗
Figure 3
Figure 3. Encode the conjunctive word equations XaX = Y ∧ aaa = XaY to one graph where X, Y are variables and a is a letter. In contrast, using an encoding that represents individual word equations while sharing global information ( [PITH_FULL_IMAGE:figures/full_fig_p022_3.png] view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: Inference rules of the proof system for word equations [PITH_FULL_IMAGE:figures/full_fig_p028_4.png]
Figure 5
Figure 5. Figure 5: The workflow diagram for the training and prediction phase. [PITH_FULL_IMAGE:figures/full_fig_p029_5.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

53 extracted references · 41 canonical work pages

  1. [1]

    DragonLi solver experimental report for benchmark a and task 2, accessed: 2025- 05-16, https://github.com/ChenchengLiang/DragonLi/tree/rank/experimental results tables/eval data GNN/A1/task 2/model

    work page 2025

  2. [2]

    The satisfiability modulo theories library (SMT-LIB), accessed: 2025-05-16, https://smtlib.cs.uiowa.edu/benchmarks.shtml

    work page 2025

  3. [3]

    Zaligvinder: A string solving benchmark framework, accessed: 2025-05-16, https://zaligvinder.github.io

    work page 2025

  4. [4]

    DragonLi github repository branch:rank (2025), accessed: 2025-05-16, https://github.com/ChenchengLiang/boosting-string-equation-solving-by- GNNs/tree/rank

    work page 2025

  5. [5]

    https://github.com/tage64/wordeq solver

    wordeq solver (2025), accessed: 2025-05-16. https://github.com/tage64/wordeq solver

    work page 2025

  6. [6]

    Abdelaziz, I., Crouse, M., Makni, B., Austil, V., Cornelio, C., Ikbal, S., Kapani- pathi, P., Makondo, N., Srinivas, K., Witbrock, M., Fokoue, A.: Learning to guide a saturation-based theorem prover (2021), https://arxiv.org/abs/2106.03906

    work page Pith review arXiv 2021

  7. [7]

    In: Akshay, S., Niemetz, A., Sankara- narayanan, S

    Abdulla, P.A., Atig, M.F., Cailler, J., Liang, C., R¨ ummer, P.: Guiding word equa- tion solving using graph neural networks. In: Akshay, S., Niemetz, A., Sankara- narayanan, S. (eds.) Automated Technology for Verification and Analysis. pp. 279–

    work page

  8. [8]

    In: Dimitrova, R., Lahav, O., Wolff, S

    Abdulla, P.A., Liang, C., R¨ ummer, P.: Boosting constrained Horn solving by unsat core learning. In: Dimitrova, R., Lahav, O., Wolff, S. (eds.) Verification, Model Checking, and Abstract Interpretation. pp. 280–302. Springer Nature Switzerland, Cham (2024)

    work page 2024

Show all 53 references
  1. [9]

    https://doi.org/10.48550/arXiv.1803.08375

    Agarap, A.F.: Deep Learning using Rectified Linear Units (ReLU) arXiv:1803.08375 (Mar 2018). https://doi.org/10.48550/arXiv.1803.08375

    2018 doi arXiv

  2. [10]

    In: Fisman, D., Rosu, G

    Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mo- hamed, A., Mohamed, M., Niemetz, A., N¨ otzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and industrial- strength SMT solver. In: Fisman, D., Ros...

    2022

  3. [11]

    CoRR abs/1806.01261 (2018), http://arxiv.org/abs/1806.01261

    Battaglia, P.W., Hamrick, J.B., Bapst, V., Sanchez-Gonzalez, A., Zambaldi, V.F., Malinowski, M., Tacchetti, A., Raposo, D., Santoro, A., Faulkner, R., G¨ ul¸ cehre, C ¸ ., Song, H.F., Ballard, A.J., Gilmer, J., Dahl, G.E., Vaswani, A., Allen, K.R., Nash, C., Langston, V., Dyer...

    2018 arXiv

  4. [12]

    In: Platzer, A., Sutcliffe, G

    B´ artek, F., Suda, M.: Neural precedence recommender. In: Platzer, A., Sutcliffe, G. (eds.) Automated Deduction – CADE 28. Lecture Notes in Computer Science, vol. 12699, pp. 503–520. Springer, Cham (2021). https://doi.org/10.1007/978-3- 030-79876-5 30, https://doi.org/10.1007...

    2021 doi

  5. [13]

    In: Piskac, R., Voronkov, A

    B´ artek, F., Suda, M.: How much should this symbol weigh? a GNN-advised clause selection. In: Piskac, R., Voronkov, A. (eds.) Proceedings of 24th In- ternational Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol. 94, pp....

    2023 doi

  6. [14]

    Chen, T., Hague, M., Lin, A.W., R¨ ummer, P., Wu, Z.: Decision procedures for path feasibility of string-manipulating programs with complex operations. Proc. ACM 18 P. Abdulla et al. Program. Lang. 3(POPL), 49:1–49:30 (2019). https://doi.org/10.1145/3290362, https://doi.org/10...

    2019 doi

  7. [15]

    In: Finkbeiner, B., Kov´ acs, L

    Chen, Y.F., Chocholat´ y, D., Havlena, V., Hol ´ ık, L., Leng´ al, O., S ´ ıˇ c, J.: Z3-noodler: An automata-based string solver. In: Finkbeiner, B., Kov´ acs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 24–33. Springer Nature Switzerland, ...

    2024

  8. [16]

    In: Filiot, E., Jungers, R., Potapov, I

    Day, J.D., Ehlers, T., Kulczynski, M., Manea, F., Nowotka, D., Poulsen, D.B.: On solving word equations using SAT. In: Filiot, E., Jungers, R., Potapov, I. (eds.) Reachability Problems. pp. 93–106. Springer International Publishing, Cham (2019)

    2019

  9. [17]

    In: Proceedings of the 8th International Con- ference on Formal Methods in Software Engineering

    Day, J.D., Kulczynski, M., Manea, F., Nowotka, D., Poulsen, D.B.: Rule- based word equation solving. In: Proceedings of the 8th International Con- ference on Formal Methods in Software Engineering. p. 87–97. FormaliSE ’20, Association for Computing Machinery, New York, NY, USA...

    2020

  10. [18]

    In: Pandya, P.K., Radhakrishnan, J

    Diekert, V., Lohrey, M.: Word equations over graph products. In: Pandya, P.K., Radhakrishnan, J. (eds.) FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science. pp. 156–167. Springer Berlin Heidelberg, Berlin, Heidelberg (2003)

    2003

  11. [19]

    CoRR abs/1704.01212 (2017), http://arxiv.org/abs/1704.01212

    Gilmer, J., Schoenholz, S.S., Riley, P.F., Vinyals, O., Dahl, G.E.: Neu- ral message passing for quantum chemistry. CoRR abs/1704.01212 (2017), http://arxiv.org/abs/1704.01212

    2017 arXiv

  12. [20]

    MIT Press, Cambridge, MA, USA (2016), http://www.deeplearningbook.org

    Goodfellow, I.J., Bengio, Y., Courville, A.: Deep Learning. MIT Press, Cambridge, MA, USA (2016), http://www.deeplearningbook.org

    2016

  13. [21]

    Journal of Symbolic Logic 16(1), 14–21 (1951)

    Horn, A.: On sentences which are true of direct unions of algebras. Journal of Symbolic Logic 16(1), 14–21 (1951). https://doi.org/10.2307/2268661

    1951 doi

  14. [22]

    In: 2021 IEEE 33rd International Conference on Tools with Artificial Intelligence (ICTAI)

    H ˚ ula, J., Mojˇ z ´ ıˇ sek, D., Janota, M.: Graph neural networks for schedul- ing of SMT solvers. In: 2021 IEEE 33rd International Conference on Tools with Artificial Intelligence (ICTAI). pp. 447–451 (2021). https://doi.org/10.1109/ICTAI52525.2021.00072

    2021

  15. [23]

    In: Peltier, N., Sofronie-Stokkermans, V

    Jakub ˚ uv, J., Chvalovsk´ y, K., Olˇ s´ ak, M., Piotrowski, B., Suda, M., Urban, J.: ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (Sys- tem Description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning. IJCAR 2020. Lecture Notes in Compu...

    2020 doi

  16. [24]

    Je˙ z, A.: Recompression: a simple and powerful technique for word equations (2014), https://arxiv.org/abs/1203.3705

    2014 arXiv

  17. [25]

    In: 5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings

    Kipf, T.N., Welling, M.: Semi-supervised classification with graph convolutional networks. In: 5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings. OpenRe- view.net (2017), https://openreview.net/...

    2017

  18. [26]

    In: Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, October 19-22, 2021

    Kumar, A., Manolios, P.: Mathematical programming modulo strings. In: Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, October 19-22, 2021. pp. 261–270. IEEE (2021). https://doi.org/10.34727/2021/ISBN.978-3-85448-046-4 36, https://doi.org/10.34727/2021/...

    2021 doi

  19. [27]

    Levi, F.W.: On semigroups. Bull. Calcutta Math. Soc 36(141-146), 82 (1944)

    1944

  20. [28]

    In: Konev, B., Schon, C., Steen, A

    Liang, C., R¨ ummer, P., Brockschmidt, M.: Exploring representation of horn clauses using GNNs. In: Konev, B., Schon, C., Steen, A. (eds.) Proceedings of the Work- When GNNs Met a Word Equations Solver 19 shop on Practical Aspects of Automated Reasoning Co-located with the 11t...

    2022

  21. [29]

    Makanin, G.S.: The problem of solvability of equations in a free semigroup. Math. Sb. (N.S.) 103(145)(2(6)), 147–236 (1977)

    1977

  22. [30]

    IEEE Trans

    Marques-Silva, J., Sakallah, K.A.: Grasp: A search algorithm for propo- sitional satisfiability. IEEE Trans. Computers 48, 506–521 (1999), https://api.semanticscholar.org/CorpusID:13039801

    1999

  23. [31]

    In: 2008 Tools and Algo- rithms for Construction and Analysis of Systems

    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: 2008 Tools and Algo- rithms for Construction and Analysis of Systems. pp. 337–340. Springer, Berlin, Heidelberg (March 2008)

    2008

  24. [32]

    Mathematische Annalen 78, 385–397 (1917), https://api.semanticscholar.org/CorpusID:119726936

    Nielsen, J.: Die Isomorphismen der allgemeinen, unendlichen Gruppe mit zwei Erzeugenden. Mathematische Annalen 78, 385–397 (1917), https://api.semanticscholar.org/CorpusID:119726936

    1917

  25. [33]

    Elsevier (2004), https://hal.science/hal-00112831

    Pin, J.E., Perrin, D.: Infinite Words: Automata, Semigroups, Logic and Games. Elsevier (2004), https://hal.science/hal-00112831

    2004

  26. [34]

    In: 40th Annual Symposium on Foundations of Computer Science (Cat

    Plandowski, W.: Satisfiability of word equations with constants is in PSPACE. In: 40th Annual Symposium on Foundations of Computer Science (Cat. No.99CB37039). pp. 495–500 (1999). https://doi.org/10.1109/SFFCS.1999.814622

    1999

  27. [35]

    CoRR abs/1308.5858 (2013), http://arxiv.org/abs/1308.5858

    Power, J.F.: Thue’s 1914 paper: a translation. CoRR abs/1308.5858 (2013), http://arxiv.org/abs/1308.5858

    2013 arXiv

  28. [36]

    CoRR abs/1903.04671 (2019)

    Selsam, D., Bjørner, N.: Neurocore: Guiding high-performance SAT solvers with unsat-core predictions. CoRR abs/1903.04671 (2019)

    2019 arXiv

  29. [37]

    In: 7th International Conference on Learn- ing Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019

    Selsam, D., Lamm, M., B¨ unz, B., Liang, P., de Moura, L., Dill, D.L.: Learning a SAT solver from single-bit supervision. In: 7th International Conference on Learn- ing Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenRe- view.net (2019), https://openreview...

    2019

  30. [38]

    In: Bengio, S., Wallach, H., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R

    Si, X., Dai, H., Raghothaman, M., Naik, M., Song, L.: Learning loop invariants for program verification. In: Bengio, S., Wallach, H., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) Advances in Neural Information Processing Systems. vol. 31. Curran Associates...

    2018

  31. [39]

    In: Computer Aided Verification: 32nd International Con- ference, CA V 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part II

    Si, X., Naik, A., Dai, H., Naik, M., Song, L.: Code2inv: A deep learning framework for program verification. In: Computer Aided Verification: 32nd International Con- ference, CA V 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part II. p. 151–164. Springer-Verlag, ...

    2020

  32. [40]

    In: Platzer, A., Sutcliffe, G

    Suda, M.: Improving enigma-style clause selection while learning from history. In: Platzer, A., Sutcliffe, G. (eds.) Automated Deduction – CADE 28. pp. 543–561. Springer International Publishing, Cham (2021)

    2021

  33. [41]

    In: 6th International Conference on Learning Representations (ICLR 2018), Vancouver, Canada, April 30 – May 3

    Veliˇ ckovi´ c, P., Cucurull, G., Casanova, A., Romero, A., Li` o, P., Bengio, Y.: Graph attention networks. In: 6th International Conference on Learning Representations (ICLR 2018), Vancouver, Canada, April 30 – May 3. OpenReview.net (2018), https://openreview.net/forum?id=rJXMpikCZ

    2018

  34. [42]

    In: Proceedings of the 31st International Conference on Neural Information Processing Systems

    Wang, M., Tang, Y., Wang, J., Deng, J.: Premise selection for theorem proving by deep graph embedding. In: Proceedings of the 31st International Conference on Neural Information Processing Systems. pp. 2783––2793. NIPS’17, Curran Asso- ciates Inc., Red Hook, NY, USA (2017)

    2017

  35. [43]

    Single equation

    Xu, K., Hu, W., Leskovec, J., Jegelka, S.: How powerful are graph neu- ral networks? In: 7th International Conference on Learning Representations (ICLR 2019), New Orleans, USA, May 6 – 9. OpenReview.net (2019), https://openreview.net/forum?id=ryGs6iA5Km 20 P. Abdulla et al. A ...

    2019

  36. [45]

    Shortest paths from SAT and UNSAT problems solved by our solver

  37. [46]

    MUSes extracted by our solver

  38. [47]

    MUSes provided by other solvers

  39. [48]

    GNN” in Table 2. The columns “3

    Shortest paths from UNSAT problems solved by our solver, guided by MUSes from other solvers. We experimented with all combinations of these sources and ultimately re- ported only the most effective one in Section 4.1. The best-performing com- bination includes MUSes from other...

  40. [49]

    Abdulla et al

    Goal 26 P. Abdulla et al. – Paper [7] : Guides the branching process, which is crucial for solving individual SAT word equations. – This paper : Guides the ranking process before branching, which signif- icantly impacts solving UNSAT word equation systems

  41. [50]

    – This paper : Uses MUSes provided by other solvers and shortest paths from UNSAT problems

    T raining Data Collection – Paper [7] : Uses shortest paths from SAT problems. – This paper : Uses MUSes provided by other solvers and shortest paths from UNSAT problems

  42. [51]

    – This paper : Encodes single word equations with syntax trees enhanced by additional global information

    W ord Equation Graph Encoding – Paper [7] : Encodes single word equations based on their syntax trees. – This paper : Encodes single word equations with syntax trees enhanced by additional global information

  43. [52]

    – This paper : Performs three different classification tasks on embeddings of word equation systems

    T raining T ask (Model Structure) – Paper [7] : Performs a multi-class classification task on single word equa- tion embeddings. – This paper : Performs three different classification tasks on embeddings of word equation systems

  44. [53]

    – This paper : Uses predictions at varying frequencies, controlled by man- ually defined criteria, including a random mechanism

    Integration into the Solver – Paper [7] : Uses predictions directly or in combination with random branching. – This paper : Uses predictions at varying frequencies, controlled by man- ually defined criteria, including a random mechanism. In summary, Paper [7] addresses branchi...

  45. [301]

    Springer Nature Switzerland, Cham (2025)

    2025

Pith tools

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