Pith. sign in

REVIEW 4 major objections 5 minor 53 references

Guiding Word Equation Solving using Graph Neural Networks (Extended Technical Report)

T0 review · 4 major / 5 minor · reviewed 2026-08-12 · deepseek-v4-flash

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

Pith's one-line read The paper claims that a graph neural network can learn which child of a Nielsen split to explore first, and that this guidance lets a basic split-based solver solve 115% more satisfiable word equations than without guidance.

desk verdict Genuinely new GNN-guided word equation solving with shipped code, but the uniform-improvement claim is contradicted by the paper's own table and the main gain may be a test-set selection artifact. read the letter →

arxiv 2411.15194 v1 pith:HRWUKU2I submitted 2024-11-19 cs.LG cs.AIcs.CLcs.LO

Parosh Aziz Abdulla , Mohamed Faouzi Atig , Julie Cailler , Chencheng Liang , Philipp Rümmer This is my paper · ORCID
classification cs.LGcs.AIcs.CLcs.LO MSC 68T0768Q4220M05
keywords wordequationsgraphneuralnetworksNielsentransformationsplitalgorithmbranchorderingstringconstraintsDragonLi
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 branch ordering is the bottleneck in Nielsen-based word equation solving and that a graph neural network can learn good branch orderings from proof trees. It introduces five graph encodings of word equations and trains a GCN to score the children of each split point, with labels derived from the size of proof subtrees under satisfiable children. If correct, this is the first deep-learning guidance for word equations, a PSPACE-hard theory where leading SMT solvers are incomplete on satisfiable instances. The strongest evidence is a single-equation benchmark where the GNN-guided solver solves 115% more satisfiable problems than its unguided counterpart and 43% more than the next best solver. On conjunctions of equations and on unsatisfiable instances, the method is competitive but not clearly ahead, because UNSAT requires exhaustive proof-tree exploration and equation order is not yet optimized.

What carries the argument

The central object is the proof tree built by the split rules R1–R9, which rewrite the first terms of each side of a word equation following the Nielsen transformation. At a branching point created by a variable-letter rule R7 or variable-variable rule R8, the algorithm must choose which child formula to expand; the GNN serves as the orderBranches heuristic, scoring each child as a multi-classification task. Training labels come from complete proof trees of satisfiable formulas: a child is positive if it is SAT and its proof subtree has minimum size among SAT children, making subtree size the proxy for how quickly a solution is found. The GNN is a two-layer graph convolutional network, and five graph encodings of word equations map the current equation and its child formulas into node-and-edge structures fed to the model.

What would settle it

Measure wall-clock time to the first SAT leaf for each branch on a sample of solved instances and compare it with proof-subtree size; if the ranking by subtree size does not correlate with time-to-SAT, the training signal is not optimizing what it claims. A second check is to retrain with labels set to actual solving time and see whether Benchmark 2 solved counts improve; if they do not, the current labeling is not the cause of the gain.

Watch

Extended reading notes

Core claim

On the paper's own terms, the discovery is that the choice of which branch to explore at each split of the Nielsen-based proof tree is learnable, and that a message-passing GCN trained on proof trees can rank branches well enough to make a from-scratch split solver beat established string solvers on satisfiable single equations. The best configuration (backtracking strategy BT2, exclusive GNN ordering, and a graph encoding with unique nodes for both variables and letters) solves 71 satisfiable problems in Benchmark 2, versus 33 for fixed-order and 41 for random-order search, and 43% more than the next best solver. Across all four benchmarks, GNN guidance uniformly improves SAT solving compared with the unguided split algorithm, though average solving time is not improved because graph encoding and model inference add overhead.

Load-bearing premise

The load-bearing premise is that the size of the proof subtree under a satisfiable child measures how fast a solution will be found down that branch, and that a GNN trained on proof trees from the unguided split algorithm generalizes to held-out equations from the same benchmark families.

Editorial extensions

If this is right

  • GNN guidance can act as a standalone branch-ordering heuristic: the exclusive-GNN strategy (S1) outperforms mixing with fixed or random orders in most experiments.
  • For single word equations and satisfiable instances, a simple split-based solver with learned branch ordering can surpass established string solvers on solved-problem counts.
  • The proof-system-plus-GNN design is modular: replacing the graph encoding or backtracking strategy changes performance, with the most informative encoding (unique variable and letter nodes) giving the best results.
  • UNSAT solving is not improved because proving unsatisfiability requires exhausting the proof tree, making branch order irrelevant; future gains would need length or automata reasoning.
  • Conjunction handling is a bottleneck: since equation order is fixed, adding a learned ranking for which equation to split first is the paper's stated next step.

Reading between the lines

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

  • If proof-subtree size is a reliable proxy for search effort, the same training scheme could be ported to other rewrite-based proof systems, such as string solvers with length reasoning, where branch order also matters.
  • Combining the GNN's branch ranking with a cheap fallback that skips graph encoding when the model is uncertain could preserve the solved-count gain while reducing per-split overhead; the paper does not test this.
  • The method's gains are demonstrated on synthetic benchmark families; Benchmark 4 (transformed SMT-LIB) shows smaller SAT gains, so distribution shift to genuinely different real-world equations is an open risk.
  • An immediate testable extension is to use the GNN scores to weight the depth limit in the complete iterative-deepening strategy (BT3), which the paper reports as relatively inefficient under fixed timeout; learned weights might make complete search practical.
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

4 major / 5 minor

Summary. The paper presents DragonLi, a word equation solver that guides branch ordering in a Nielsen/split-based proof search with a Graph Convolutional Network. The authors define a proof system for word equations, propose five graph encodings of equations, train a GNN on labels derived from proof-tree subtree sizes, and integrate the predictions into the orderBranches function. Experiments on four benchmarks compare the fixed, random, and GNN-guided versions of DragonLi against cvc5, Z3, Z3-Noodler, Ostrich, and Woorpje. The central claim is that GNN guidance uniformly improves SAT solving and that the GNN-guided version solves 115% more SAT problems than the non-GNN-guided version on Benchmark 2.

Significance. If the reported gains are robust, this is a useful new direction for a PSPACE-hard theory where leading SMT solvers are often incomplete on satisfiable instances, and it appears to be the first deep-learning-based branch guidance for word equations. The paper contributes a clean proof system with soundness and local-completeness arguments, five graph representations, a 45-configuration ablation study, and a public artifact on GitHub/Zenodo. These are genuine strengths. The central experimental claim, however, is currently not established because the configuration-selection protocol is internally inconsistent and the 'uniform improvement' statement is contradicted by the paper's own Table 2.

major comments (4)
  1. [Section 5.4, Table 2, Table 3] The text says the GNN row in Table 2 is 'selected from the best results out of 45 experiments', while the caption of Table 2 says all GNN rows share the configuration (BT2, S1, G5). These statements are incompatible. Table 3 shows, for example, that the best Benchmark 1 SAT count is 1000 and the best Benchmark 3 SAT count is 35 (G4, BT1, S1), but Table 2 reports 995 and 32 for the shared configuration. If the intended protocol is to take the maximum over 45 configurations on the same evaluation set, then the headline Benchmark 2 result (71 vs Fixed 33) is a selection maximum and not a reliable estimate of the configuration's expected performance. The paper reports no validation split, no repeated-seed statistics, and no multiple-comparison control, so the magnitude of the GNN benefit is not established.
  2. [Section 1, Table 2] The claim that enabling GNN guidance 'uniformly improves performance on SAT problems' is contradicted by the paper's own data. In Benchmark 1, GNN solves 995 SAT problems versus 999 for the fixed-order version; in Benchmark 3, GNN solves 32 versus Fixed 32; and in Benchmark 4, GNN solves 418 versus Fixed 416, a difference of two problems. The uniform-improvement statement should be removed or replaced with a per-benchmark comparison that includes uncertainty or significance information.
  3. [Section 4.3] The training labels use the proof-subtree size Delta(v) to decide which child 'leads to a solution more quickly', but the paper never validates that subtree size correlates with actual solving time. The labels are generated by the unguided split algorithm, whereas the guided solver changes branch order; the transfer of learned rankings under this distribution shift is assumed rather than tested. Because the Benchmark 2 gain is attributed entirely to these rankings, the label proxy is load-bearing and should be validated, for instance by comparing predicted branch rankings against measured solving times on held-out instances. The rule that arbitrarily discards extra positive labels until exactly one child is marked positive also injects label noise that is not analyzed.
  4. [Section 1, Table 2] The numerical claim that GNN-guided DragonLi solves '43.0% more than the next best string solver, Woorpje' is inconsistent with Table 2, where Woorpje solves 23 SAT problems and GNN solves 71 SAT problems on Benchmark 2. That is an increase of about 209%, not 43.0%. All percentage claims in the abstract and introduction should be recomputed against the final reported table.
minor comments (5)
  1. [Section 5.4] The text refers to the 'orderRules' function, but Algorithm 2 defines the function as 'orderBranches'; the terminology should be consistent.
  2. [Table 2] The table header contains 'split numbet' and the GNN row for Benchmark 3 appears to contain a duplicated '1471.2' entry; these formatting errors should be corrected.
  3. [Table 1] The layout of Table 1 is hard to parse because the Total, Eval, SAT, UNSAT, and UNKNOWN counts are run together in a single row of numbers; separate columns or subheaders would improve readability.
  4. [Section 5.3] The experimental settings list hidden-layer size and message-passing layers but omit GNN training details such as learning rate, batch size, number of epochs, and random seeds; these should be stated in the paper or explicitly pointed to in the Zenodo artifact.
  5. [Section 4.4] The stochastic strategies Random, S2, and S3 are evaluated without reporting seeds or repeated runs, so the random baselines are not reproducible and their variance is unknown.

Circularity Check

1 steps flagged · score 5.0 of 10

Headline Benchmark 2 gain is a test-set maximum over 45 configurations, not an independent held-out prediction; the formal derivation itself is self-contained.

  1. fitted input called prediction [Section 5.4, Table 2 caption, Section 5.2, Table 3]
    ""The performance of the GNN-guided DragonLi (row GNN in Table 2) for each benchmark is selected from the best results out of 45 experiments (see Table 3)" ... "GNN rows for benchmarks 1-4 share the configuration ( BT2, S1, G5)" ... "those sets were exclusively used for evaluation, not for training or for tuning hyper-parameters.""

    Benchmark 2's GNN row (71 SAT solved) equals the maximum of all 45 configurations in Table 3 (Graph 5, BT2, S1). Section 5.4 says the row is 'selected from the best results out of 45 experiments', so the headline 115% improvement over Fixed (33) is the maximum over 45 models evaluated on the same 1000-problem set that Section 5.2 says was 'exclusively used for evaluation, not for training or for tuning hyper-parameters.' Selecting the best of 45 test-set outcomes and reporting it as 'the GNN-guided version' statistically forces the result upward: under a null hypothesis of no benefit, the maximum of 45 configurations exceeds a single fixed baseline.

full rationale

No significant circularity in the formal derivation: Lemma 1 proves soundness and local completeness of the proof rules directly, and Lemma 2 derives Algorithm 1's correctness from Lemma 1 without relying on GNN behaviour. The GNN training labels are generated from proof trees of the unguided split algorithm (Section 4.3), but this is not a definitional cycle because evaluation is on held-out problems and measures real solved counts with a timeout; the learned heuristic could in principle fail to transfer. The main circularity concern is in the evaluation, not the derivation: the headline Benchmark 2 result is the best of 45 configurations selected on the evaluation set, contradicting the paper's statement that evaluation sets were not used for tuning. This makes the reported magnitude of the GNN improvement partly constructed by the selection procedure, although the ablation table shows several GNN configurations independently outperform the fixed baseline on Benchmark 2, so the central claim retains independent content. Overall score 5.

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

The central empirical claim rests on hand-chosen search limits and architecture sizes, plus a labeling proxy (minimal subtree size) that is not validated against time. The fresh variables introduced in split rules R7/R8 are standard proof-system devices, not postulated entities. The axioms are standard word equation semantics and benchmark representativeness assumptions.

free parameters (6)
  • backtrack depth limit lBT2 = 500
    Hand-chosen in Section 5.3; controls how deep BT2 search goes before backtracking, affecting solved counts and runtime.
  • backtrack depth increment lstep_BT2 = 250
    Hand-chosen increment for BT2 in Section 5.3.
  • initial depth limit lBT3 = 20
    Hand-chosen initial iterative-deepening limit in Section 5.3.
  • GNN hidden layer size = 128
    Architecture choice, Section 5.3.
  • GNN message-passing layers = 2
    Architecture choice, Section 5.3.
  • branch label proxy = minimal subtree size Delta(v)
    Section 4.3 uses subtree size, not measured solving time, to label which branch is best; this proxy is a modeling choice that the GNN learns.
assumptions (4)
  • standard math The split proof rules R1-R9 are sound and locally complete.
    Lemma 1; proof given as an outline in Appendix A, relies on standard Nielsen transformation properties.
  • domain assumption The benchmark generation mechanisms produce word equations that are representative of real-world or hard instances.
    Benchmarks 1-3 are artificial, adapted from Woorpje; Benchmark 4 is filtered from SMT-LIB but transformed, so satisfiability labels may change. Section 5.2.
  • ad hoc to paper Subtree size is a reliable proxy for solution-finding time.
    Section 4.3 labels branches by minimal subtree size among SAT children; this is the target quantity the GNN learns and is not validated against actual solving time.
  • domain assumption A GNN trained on proof trees of the unguided split algorithm can produce branch orderings that generalize to held-out equations.
    The training distribution matches the evaluation benchmarks; generalization to other distributions is not demonstrated. Sections 4.2-4.3 and 5.2.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Guiding Word Equation Solving using Graph Neural Networks (Extended Technical Report)." pith.science (2026). https://pith.science/paper/HRWUKU2I

@misc{pith2026241115194,
  author       = {Pith},
  title        = {Pith review of: Guiding Word Equation Solving using Graph Neural Networks (Extended Technical Report)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/HRWUKU2I}},
  note         = {Machine review of arXiv:2411.15194}
}
read the original abstract

This paper proposes a Graph Neural Network-guided algorithm for solving word equations, based on the well-known Nielsen transformation for splitting equations. The algorithm iteratively rewrites the first terms of each side of an equation, giving rise to a tree-like search space. The choice of path at each split point of the tree significantly impacts solving time, motivating the use of Graph Neural Networks (GNNs) for efficient split decision-making. Split decisions are encoded as multi-classification tasks, and five graph representations of word equations are introduced to encode their structural information for GNNs. The algorithm is implemented as a solver named DragonLi. Experiments are conducted on artificial and real-world benchmarks. The algorithm performs particularly well on satisfiable problems. For single word \mbox{equations}, DragonLi can solve significantly more problems than well-established string solvers. For the conjunction of multiple word equations, DragonLi is competitive with state-of-the-art string solvers.

Figures

Figures reproduced from arXiv: 2411.15194 by the authors.

Figure 1
Figure 1. The workflow diagram for the training and prediction stage [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Rules of the proof system for word equations [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. Proof tree resulting from the word equation [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: The five graph representations for the word equation [PITH_FULL_IMAGE:figures/full_fig_p011_4.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

53 extracted references · 21 canonical work pages

  1. [1]

    The satisfiability modulo theories library (SMT-LIB), accessed: 2024-04-25, https: //smtlib.cs.uiowa.edu/benchmarks.shtml

    work page 2024

  2. [2]

    https://github.com/ ChenchengLiang/boosting-string-equation-solving-by-GNNs

    DragonLi github repository (2024), accessed: 2024-06-28. https://github.com/ ChenchengLiang/boosting-string-equation-solving-by-GNNs

    work page 2024

  3. [3]

    https://zenodo.org/ records/13354774

    Zenodo record of DragonLi (2024), accessed: 2024-08-21. https://zenodo.org/ records/13354774

    work page arXiv 2024

  4. [4]

    In: Biere, A., Bloem, R

    Abdulla, P.A., Atig, M.F., Chen, Y.F., Hol ´ ık, L., Rezine, A., R¨ ummer, P., Stenman, J.: String constraints for verification. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification. pp. 150–166. Springer International Publishing, Cham (2014)

    work page 2014

  5. [5]

    In: Kroening, D., P˘ as˘ areanu, C.S

    Abdulla, P.A., Atig, M.F., Chen, Y.F., Hol ´ ık, L., Rezine, A., R¨ ummer, P., Sten- man, J.: Norn: An SMT solver for string constraints. In: Kroening, D., P˘ as˘ areanu, C.S. (eds.) Computer Aided Verification. pp. 462–469. Springer International Pub- lishing, Cham (2015)

    work page 2015

  6. [6]

    In: 2018 Formal Methods in Computer Aided Design (FMCAD)

    Abdulla, P.A., Faouzi Atig, M., Chen, Y.F., Diep, B.P., Hol ´ ık, L., Rezine, A., R¨ ummer, P.: TRAU: SMT solver for string constraints. In: 2018 Formal Methods in Computer Aided Design (FMCAD). pp. 1–5 (2018). https://doi.org/10.23919/FMCAD.2018.8602997

    arXiv 2018

  7. [7]

    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)

    2024

  8. [8]

    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

    arXiv doi:10.48550/arxiv.1803.08375 2018

Show all 53 references
  1. [9]

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

    Allamanis, M., Brockschmidt, M., Khademi, M.: Learning to represent programs with graphs. CoRR abs/1711.00740 (2017), http://arxiv.org/abs/1711.00740

    2017 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]

    In: Gopalakrishnan, G., Qadeer, S

    Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi´ c, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) Com- puter Aided Verification. pp. 171–177. Springer Berlin Heidelberg, Berlin, Heidel- berg (2011)

    2011

  4. [12]

    Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Tech. rep., Department of Computer Science, The University of Iowa (2017), available at www.SMT-LIB.org

    2017

  5. [13]

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

    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

  6. [14]

    In: 2017 Formal Methods in Computer Aided Design (FMCAD)

    Berzish, M., Ganesh, V., Zheng, Y.: Z3str3: A string solver with theory-aware heuristics. In: 2017 Formal Methods in Computer Aided Design (FMCAD). pp. 55–59 (2017). https://doi.org/10.23919/FMCAD.2017.8102241 22 P. Abdulla et al

    2017

  7. [15]

    In: Proceed- ings of the Fourth International Workshop on Data Management for End-to- End Machine Learning

    Chen, A., Chow, A., Davidson, A., DCunha, A., Ghodsi, A., Hong, S.A., Kon- winski, A., Mewald, C., Murching, S., Nykodym, T., Ogilvie, P., Parkhe, M., Singh, A., Xie, F., Zaharia, M., Zang, R., Zheng, J., Zumar, C.: Developments in mlflow: A system to accelerate the machine le...

    2020

  8. [16]

    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 Program. Lang. 3(POPL), 49:1–49:30 (2019). https://doi.org/10.1145/3290362, https://doi.org/10.1145/3290362

    2019 doi

  9. [17]

    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

  10. [18]

    In: Piskac, R., Voronkov, A

    Chvalovsky, K., Korovin, K., Piepenbrock, J., Urban, J.: Guiding an instanti- ation prover with graph neural networks. In: Piskac, R., Voronkov, A. (eds.) Proceedings of 24th International Conference on Logic for Programming, Arti- ficial Intelligence and Reasoning. EPiC Serie...

  11. [19]

    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

  12. [20]

    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

  13. [21]

    Ellson, J., Gansner, E.R., Koutsofios, E., North, S.C., Woodhull, G.: Graphviz and Dynagraph — Static and Dynamic Graph Drawing Tools, pp. 127–148. Springer Berlin Heidelberg, Berlin, Heidelberg (2004). https://doi.org/10.1007/978-3-642- 18638-7 6, https://doi.org/10.1007/978-...

    2004 doi

  14. [22]

    In: The World Wide Web Conference

    Fan, W., Ma, Y., Li, Q., He, Y., Zhao, E., Tang, J., Yin, D.: Graph neural networks for social recommendation. In: The World Wide Web Conference. pp. 417–426. WWW ’19, Association for Computing Machinery, New York, NY, USA (2019). https://doi.org/10.1145/3308558.3313488

    2019

  15. [23]

    In: Proceedings of the 34th International Con- ference on Machine Learning - Volume 70

    Gilmer, J., Schoenholz, S.S., Riley, P.F., Vinyals, O., Dahl, G.E.: Neural message passing for Quantum chemistry. In: Proceedings of the 34th International Con- ference on Machine Learning - Volume 70. pp. 1263–1272. ICML’17, JMLR.org (2017)

    2017

  16. [24]

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

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

    2017 arXiv

  17. [25]

    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

  18. [26]

    In: Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics

    Harrison, J.: Hol light: An overview. In: Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics. pp. 60–66. TPHOLs ’09, Springer-Verlag, Berlin, Heidelberg (2009) Title Suppressed Due to Excessive Length 23

    2009

  19. [27]

    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

  20. [28]

    In: 2018 For- mal Methods in Computer Aided Design (FMCAD)

    Hojjat, H., R¨ ummer, P.: The ELDARICA Horn solver. In: 2018 For- mal Methods in Computer Aided Design (FMCAD). pp. 1–7 (2018). https://doi.org/10.23919/FMCAD.2018.8603013

    2018

  21. [29]

    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 (system de- scription). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning. pp. 448–463. Springer Internationa...

    2020

  22. [30]

    Khmelevskii, Y.I.: Equations in a free semigroup. Proc. Steklov Inst. Math. 107, 1–270 (1971)

    1971

  23. [31]

    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

  24. [32]

    Artificial Intelligence 27(1), 97–109 (1985)

    Korf, R.E.: Depth-First Iterative-Deepening: An Optimal Admissible Tree Search. Artificial Intelligence 27(1), 97–109 (1985)

    1985

  25. [33]

    net/forum?id=B1lCn64tvS

    Kurin, V., Godil, S., Whiteson, S., Catanzaro, B.: Improving SAT solver heuris- tics with graph networks and reinforcement learning (2020),https://openreview. net/forum?id=B1lCn64tvS

    2020

  26. [34]

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

    1944

  27. [35]

    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 Workshop on Practical Aspects of Automated Reasoning Co-located with the 11th Inter- national Joint Conference on Autom...

    2022

  28. [36]

    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

  29. [37]

    IEEE Trans

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

    1999

  30. [38]

    In: Proceedings of the Thir- tieth AAAI Conference on Artificial Intelligence

    Mou, L., Li, G., Zhang, L., Wang, T., Jin, Z.: Convolutional neural networks over tree structures for programming language processing. In: Proceedings of the Thir- tieth AAAI Conference on Artificial Intelligence. pp. 1287–1293. AAAI’16, AAAI Press (2016)

    2016

  31. [39]

    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

  32. [40]

    Mathematische Annalen 78, 385–397 (1917), https://api

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

    1917

  33. [41]

    CoRR abs/1905.10006 (2019)

    Paliwal, A., Loos, S.M., Rabe, M.N., Bansal, K., Szegedy, C.: Graph representa- tions for higher-order logic and theorem proving. CoRR abs/1905.10006 (2019)

    2019 arXiv

  34. [42]

    Abdulla et al

    Paszke, A., Gross, S., Massa, F., Lerer, A., Bradbury, J., Chanan, G., Killeen, T., Lin, Z., Gimelshein, N., Antiga, L., Desmaison, A., Kopf, A., Yang, E., DeVito, Z., Raison, M., Tejani, A., Chilamkurthy, S., Steiner, B., Fang, L., Bai, J., Chintala, S.: Pytorch: An imperativ...

    2019

  35. [43]

    In: Proceedings of the 25th International Conference on World Wide Web

    Pezoa, F., Reutter, J.L., Suarez, F., Ugarte, M., Vrgoˇ c, D.: Foundations of json schema. In: Proceedings of the 25th International Conference on World Wide Web. pp. 263–273. International World Wide Web Conferences Steering Committee (2016)

    2016

  36. [44]

    In: Proceed- ings of the Thirty-Eighth Annual ACM Symposium on Theory of Computing

    Plandowski, W.: An efficient algorithm for solving word equations. In: Proceed- ings of the Thirty-Eighth Annual ACM Symposium on Theory of Computing. pp. 467—-476. STOC ’06, Association for Computing Machinery, New York, NY, USA (2006). https://doi.org/10.1145/1132516.1132584

    2006

  37. [45]

    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

  38. [46]

    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

  39. [47]

    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

  40. [48]

    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

  41. [49]

    CreateSpace, Scotts Valley, CA (2009)

    Van Rossum, G., Drake, F.L.: Python 3 Reference Manual. CreateSpace, Scotts Valley, CA (2009)

    2009

  42. [50]

    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

  43. [51]

    arXiv preprint arXiv:1909.01315 (2019)

    Wang, M., Zheng, D., Ye, Z., Gan, Q., Li, M., Song, X., Zhou, J., Ma, C., Yu, L., Gai, Y., Xiao, T., He, T., Karypis, G., Li, J., Zhang, Z.: Deep graph library: A graph-centric, highly-performant package for graph neural networks. arXiv preprint arXiv:1909.01315 (2019)

    2019 arXiv

  44. [52]

    CoRR abs/2110.14053 (2021), https://arxiv.org/abs/2110.14053 Title Suppressed Due to Excessive Length 25 A Proof of Lemma 1 Proof

    Wang, W., Hu, Y., Tiwari, M., Khurshid, S., McMillan, K.L., Miikkulainen, R.: Neurocomb: Improving SAT solving with graph neural networks. CoRR abs/2110.14053 (2021), https://arxiv.org/abs/2110.14053 Title Suppressed Due to Excessive Length 25 A Proof of Lemma 1 Proof. Outline...

    2021 arXiv

  45. [123]

    https://doi.org/10.29007/tp23, https://easychair.org/ publications/paper/5z94

    EasyChair (2023). https://doi.org/10.29007/tp23, https://easychair.org/ publications/paper/5z94

    2023 doi

Pith tools

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