{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T13:06:42Z","timestamp":1762088802857,"version":"build-2065373602"},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Clause selection plays a crucial role in modern saturation-based automatic theorem provers. A commonly used heuristic suggests prioritizing small clauses, i.e., clauses with few symbol occurrences. More generally, we can give preference to clauses with a low weighted symbol occurrence count, where each symbol\u2019s occurrence count is multiplied by a respective symbol weight. Traditionally, a human domain expert would supply the symbol weights.<\/jats:p><jats:p>In this paper, we propose a system based on a graph neural network that learns to predict symbol weights with the aim of improving clause selection for arbitrary first-order logic problems. Our experiments demonstrate that by advising the automatic theorem prover Vampire on the first-order fragment of TPTP using a trained neural network, the prover\u2019s problem solving capability improves by 6.6% compared to uniformly weighting symbols and by 2.1% compared to a goal-directed variant of the uniformly weighting strategy.<\/jats:p>","DOI":"10.29007\/5f4r","type":"proceedings-article","created":{"date-parts":[[2023,6,3]],"date-time":"2023-06-03T22:10:10Z","timestamp":1685830210000},"page":"96-79","source":"Crossref","is-referenced-by-count":3,"title":["How Much Should This Symbol Weigh? A GNN-Advised Clause Selection"],"prefix":"10.29007","volume":"94","author":[{"given":"Filip","family":"B\u00e1rtek","sequence":"first","affiliation":[]},{"given":"Martin","family":"Suda","sequence":"additional","affiliation":[]}],"member":"11545","event":{"name":"Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2023,6,3]],"date-time":"2023-06-03T22:10:15Z","timestamp":1685830215000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/2BSs"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/5f4r","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}