{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,19]],"date-time":"2026-05-19T16:53:48Z","timestamp":1779209628908,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":50,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,8,24]],"date-time":"2024-08-24T00:00:00Z","timestamp":1724457600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,8,25]]},"DOI":"10.1145\/3637528.3671627","type":"proceedings-article","created":{"date-parts":[[2024,8,25]],"date-time":"2024-08-25T04:55:12Z","timestamp":1724561712000},"page":"6301-6311","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1134-045X","authenticated-orcid":false,"given":"Zhanguang","family":"Zhang","sequence":"first","affiliation":[{"name":"Huawei Noah's Ark Lab, Montreal, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9458-6879","authenticated-orcid":false,"given":"Didier","family":"Ch\u00e9telat","sequence":"additional","affiliation":[{"name":"Huawei Noah's Ark Lab, Montreal, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-4876-2765","authenticated-orcid":false,"given":"Joseph","family":"Cotnareanu","sequence":"additional","affiliation":[{"name":"McGill University, Montreal, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-5278-0184","authenticated-orcid":false,"given":"Amur","family":"Ghose","sequence":"additional","affiliation":[{"name":"Huawei Noah's Ark Lab, Montreal, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4218-3904","authenticated-orcid":false,"given":"Wenyi","family":"Xiao","sequence":"additional","affiliation":[{"name":"Huawei Noah's Ark Lab, Hong Kong, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0310-3825","authenticated-orcid":false,"given":"Hui-Ling","family":"Zhen","sequence":"additional","affiliation":[{"name":"Huawei Noah's Ark Lab, Hong Kong, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9871-4682","authenticated-orcid":false,"given":"Yingxue","family":"Zhang","sequence":"additional","affiliation":[{"name":"Huawei Noah's Ark Lab, Montreal, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0422-8235","authenticated-orcid":false,"given":"Jianye","family":"Hao","sequence":"additional","affiliation":[{"name":"Huawei Noah's Ark Lab, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5030-1379","authenticated-orcid":false,"given":"Mark","family":"Coates","sequence":"additional","affiliation":[{"name":"McGill University, Montreal, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2236-8784","authenticated-orcid":false,"given":"Mingxuan","family":"Yuan","sequence":"additional","affiliation":[{"name":"Huawei Noah's Ark Lab, Hong Kong, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,8,24]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"Cook","author":"Applegate David L.","year":"2007","unstructured":"David L. Applegate, Robert E. Bixby, Va?ek Chv\u00e1tal, and William J. Cook. 2007. The Traveling Salesman Problem: A Computational Study. Princeton University Press."},{"key":"e_1_3_2_2_2_1","unstructured":"Tomas Balyo Marijn J. H. Heule Markus Iser Matti J\u00e4rvisalo and Martin Suda. 2022. SAT Competition. https:\/\/satcompetition.github.io\/2022"},{"key":"e_1_3_2_2_3_1","volume-title":"IsaSAT and Kissat entering the SAT Competition","author":"Biere Armin","year":"2022","unstructured":"Armin Biere and Mathias Fleury. 2022. Gimsatul, IsaSAT and Kissat entering the SAT Competition 2022. In Proc. of SAT Competition 2022 - Solver and Benchmark Descriptions (Department of Computer Science Series of Publications B, Vol. B-2022-1), Tomas Balyo, Marijn Heule, Markus Iser, Matti J\u00e4rvisalo, and Martin Suda (Eds.). University of Helsinki, 10--11."},{"key":"e_1_3_2_2_4_1","volume-title":"ASlib: A benchmark library for algorithm selection. Artificial Intelligence","author":"Bischl Bernd","year":"2016","unstructured":"Bernd Bischl, Pascal Kerschke, Lars Kotthoff, Marius Lindauer, Yuri Malitsky, Alexandre Fr\u00e9chette, Holger Hoos, Frank Hutter, Kevin Leyton-Brown, Kevin Tierney, and Joaquin Vanschoren. 2016. ASlib: A benchmark library for algorithm selection. Artificial Intelligence (2016)."},{"key":"e_1_3_2_2_5_1","first-page":"1","article-title":"Combinatorial optimization and reasoning with graph neural networks","volume":"24","author":"Cappart Quentin","year":"2023","unstructured":"Quentin Cappart, Didier Ch\u00e9telat, Elias B Khalil, Andrea Lodi, Christopher Morris, and Petar Velivckovi\u0107. 2023. Combinatorial optimization and reasoning with graph neural networks. Journal of Machine Learning Research, Vol. 24 (2023), 1--61.","journal-title":"Journal of Machine Learning Research"},{"key":"e_1_3_2_2_6_1","volume-title":"Accessed: February 8th","author":"SAT Competition Committee","year":"2009","unstructured":"SAT Competition Committee. 2009. Benchmark Submission Guidelines. http:\/\/www.satcompetition.org\/2009\/format-benchmarks2009.html. Accessed: February 8th, 2024."},{"key":"e_1_3_2_2_7_1","volume-title":"Accessed: February 8th","author":"SAT Competition Committee","year":"2023","unstructured":"SAT Competition Committee. 2023. The International SAT Competition Web Page. http:\/\/www.satcompetition.org. Accessed: February 8th, 2024."},{"key":"e_1_3_2_2_8_1","unstructured":"Stephen A Cook. 2023. The complexity of theorem-proving procedures. In Logic Automata and Computational Complexity: The Works of Stephen A. Cook. 143--152."},{"key":"e_1_3_2_2_9_1","volume-title":"Proceedings of the 2nd AAAI Conference on Artificial Intelligence. 1092--1097","author":"Crawford James M","year":"1994","unstructured":"James M Crawford and Andrew B Baker. 1994. Experimental results on the application of satisfiability algorithms to scheduling problems. In Proceedings of the 2nd AAAI Conference on Artificial Intelligence. 1092--1097."},{"key":"e_1_3_2_2_10_1","volume-title":"Proceedings of the 16th ITAT Conference Information Technologies - Applications and Theory.","author":"Degroote Hans","year":"2016","unstructured":"Hans Degroote, Bernd Bischl, Lars Kotthoff, and Patrick De Causmaecker. 2016. Reinforcement learning for automatic online algorithm selection-an empirical study. In Proceedings of the 16th ITAT Conference Information Technologies - Applications and Theory."},{"key":"e_1_3_2_2_11_1","volume-title":"Linear-time algorithms for testing the satisfiability of propositional Horn formulae. The Journal of Logic Programming","author":"Dowling William F","year":"1984","unstructured":"William F Dowling and Jean H Gallier. 1984. Linear-time algorithms for testing the satisfiability of propositional Horn formulae. The Journal of Logic Programming (1984)."},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11499107_33"},{"key":"e_1_3_2_2_13_1","first-page":"1","article-title":"Benchmarking graph neural networks","volume":"24","author":"Dwivedi Vijay Prakash","year":"2023","unstructured":"Vijay Prakash Dwivedi, Chaitanya K Joshi, Anh Tuan Luu, Thomas Laurent, Yoshua Bengio, and Xavier Bresson. 2023. Benchmarking graph neural networks. Journal of Machine Learning Research, Vol. 24, 43 (2023), 1--48.","journal-title":"Journal of Machine Learning Research"},{"key":"e_1_3_2_2_14_1","volume-title":"Artificial Intelligence","author":"Froleyks Nils","year":"2021","unstructured":"Nils Froleyks, Marijn Heule, Markus Iser, Matti J\u00e4rvisalo, and Martin Suda. 2021. SAT Competition 2020. Artificial Intelligence (2021)."},{"key":"e_1_3_2_2_15_1","volume-title":"Algorithm portfolio selection as a bandit problem with unbounded losses. Annals of Mathematics and Artificial Intelligence","author":"Gagliolo Matteo","year":"2011","unstructured":"Matteo Gagliolo and J\u00fcrgen Schmidhuber. 2011. Algorithm portfolio selection as a bandit problem with unbounded losses. Annals of Mathematics and Artificial Intelligence (2011)."},{"key":"e_1_3_2_2_16_1","volume-title":"SAT-based Scalable Formal Verification Solutions","author":"Ganai Malay","unstructured":"Malay Ganai and Aarti Gupta. 2007. SAT-based Scalable Formal Verification Solutions. Springer."},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/367072.367111"},{"key":"e_1_3_2_2_18_1","volume-title":"Deep Learning","author":"Goodfellow Ian J.","unstructured":"Ian J. Goodfellow, Yoshua Bengio, and Aaron Courville. 2016. Deep Learning. MIT Press, Cambridge, MA, USA."},{"key":"e_1_3_2_2_19_1","volume-title":"Machine learning methods in solving the Boolean satisfiability problem. Machine Intelligence Research","author":"Guo Wenxuan","year":"2023","unstructured":"Wenxuan Guo, Hui-Ling Zhen, Xijun Li, Wanqian Luo, Mingxuan Yuan, Yaohui Jin, and Junchi Yan. 2023. Machine learning methods in solving the Boolean satisfiability problem. Machine Intelligence Research (2023), 1--16."},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1561\/2200000081"},{"key":"e_1_3_2_2_21_1","volume-title":"Formal Equivalence Checking and Design Debugging","author":"Huang Shi-Yu","unstructured":"Shi-Yu Huang and Kwang-Ting Tim Cheng. 2012. Formal Equivalence Checking and Design Debugging. Vol. 12. Springer Science & Business Media."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.03.013"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/2041160.2041198"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/3087368.3087412"},{"key":"e_1_3_2_2_25_1","volume-title":"Automated algorithm selection: Survey and perspectives. Evolutionary computation","author":"Kerschke Pascal","year":"2019","unstructured":"Pascal Kerschke, Holger H Hoos, Frank Neumann, and Heike Trautmann. 2019. Automated algorithm selection: Survey and perspectives. Evolutionary computation (2019)."},{"key":"e_1_3_2_2_26_1","volume-title":"Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980","author":"Kingma Diederik P","year":"2014","unstructured":"Diederik P Kingma and Jimmy Ba. 2014. Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980 (2014)."},{"key":"e_1_3_2_2_27_1","volume-title":"Proceedings of the 5th International Conference on Learning Representations.","author":"Thomas","unstructured":"Thomas N. Kipf and Max Welling. 2017. Semi-Supervised Classification with Graph Convolutional Networks. In Proceedings of the 5th International Conference on Learning Representations."},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/3495724.3496530"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3580305.3599837"},{"key":"e_1_3_2_2_30_1","volume-title":"Autofolio: An automatically configured algorithm selector. Journal of Artificial Intelligence Research","author":"Lindauer Marius","year":"2015","unstructured":"Marius Lindauer, Holger H Hoos, Frank Hutter, and Torsten Schaub. 2015. Autofolio: An automatically configured algorithm selector. Journal of Artificial Intelligence Research (2015)."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v30i1.10170"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-44973-4_17"},{"key":"e_1_3_2_2_33_1","volume-title":"Handbook of satisfiability","author":"Marques-Silva Joao","unstructured":"Joao Marques-Silva, In\u00eas Lynce, and Sharad Malik. 2021. Conflict-driven clause learning SAT solvers. In Handbook of satisfiability. IOS press, 133--182."},{"key":"e_1_3_2_2_34_1","volume-title":"Simple algorithm portfolio for SAT. Artificial Intelligence Review","author":"Nikoli\u0107 Mladen","year":"2013","unstructured":"Mladen Nikoli\u0107, Filip Mari\u0107, and Predrag Janivci\u0107. 2013. Simple algorithm portfolio for SAT. Artificial Intelligence Review (2013)."},{"key":"e_1_3_2_2_35_1","volume-title":"Proceedings of the 32nd International Conference on Neural Information Processing Systems.","author":"Paszke Adam","year":"2019","unstructured":"Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, et al. 2019. Pytorch: An imperative style, high-performance deep learning library. In Proceedings of the 32nd International Conference on Neural Information Processing Systems."},{"key":"e_1_3_2_2_36_1","volume-title":"Scikit-learn: Machine learning in Python. the Journal of machine Learning research","author":"Pedregosa Fabian","year":"2011","unstructured":"Fabian Pedregosa, Ga\u00ebl Varoquaux, Alexandre Gramfort, Vincent Michel, Bertrand Thirion, Olivier Grisel, Mathieu Blondel, Peter Prettenhofer, Ron Weiss, Vincent Dubourg, et al. 2011. Scikit-learn: Machine learning in Python. the Journal of machine Learning research, Vol. 12 (2011), 2825--2830."},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-24258-9_24"},{"key":"e_1_3_2_2_38_1","volume-title":"Proceedings of the 7th International Conference on Learning Representations.","author":"Selsam Daniel","year":"2019","unstructured":"Daniel Selsam, Matthew Lamm, Benedikt B\u00fcnz, Percy Liang, Leonardo de Moura, and David L Dill. 2019. Learning a SAT solver from single-bit supervision. In Proceedings of the 7th International Conference on Learning Representations."},{"key":"e_1_3_2_2_39_1","volume-title":"A constraint solver for software engineering: finding models and cores of large relational specifications. Ph.,D. Dissertation","author":"Torlak Emina","unstructured":"Emina Torlak. 2009. A constraint solver for software engineering: finding models and cores of large relational specifications. Ph.,D. Dissertation. Massachusetts Institute of Technology."},{"key":"e_1_3_2_2_40_1","volume-title":"On the complexity of derivation in propositional calculus. Automation of Reasoning 2: Classical Papers on Computational Logic 1967--1970","author":"Tseitin Grigori S","year":"1983","unstructured":"Grigori S Tseitin. 1983. On the complexity of derivation in propositional calculus. Automation of Reasoning 2: Classical Papers on Computational Logic 1967--1970 (1983), 466--483."},{"key":"e_1_3_2_2_41_1","volume-title":"Proceedings of the 30th International Conference on Neural Information Processing Systems.","author":"Vaswani Ashish","year":"2017","unstructured":"Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, \u0141ukasz Kaiser, and Illia Polosukhin. 2017. Attention is all you need. In Proceedings of the 30th International Conference on Neural Information Processing Systems."},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3340531.3411963"},{"key":"e_1_3_2_2_43_1","volume-title":"ICLR Workshop on Representation Learning on Graphs and Manifolds.","author":"Wang Minjie Yu","year":"2019","unstructured":"Minjie Yu Wang. 2019. Deep Graph Library: Towards efficient and scalable deep learning on graphs. In ICLR Workshop on Representation Learning on Graphs and Manifolds."},{"key":"e_1_3_2_2_44_1","unstructured":"Weihuang Wen and Tianshu Yu. 2023. W2SAT: Learning to generate SAT instances from Weighted Literal Incidence Graphs. arxiv: 2302.00272 [cs.LG]"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_18"},{"key":"e_1_3_2_2_46_1","volume-title":"SATzilla: Portfolio-Based Algorithm Selection for SAT. Journal of Artificial Intelligence Research","author":"Xu Lin","year":"2008","unstructured":"Lin Xu, Frank Hutter, Holger H. Hoos, and Kevin Leyton-Brown. 2008. SATzilla: Portfolio-Based Algorithm Selection for SAT. Journal of Artificial Intelligence Research (2008)."},{"key":"e_1_3_2_2_47_1","unstructured":"Lin Xu Frank Hutter Holger H Hoos and Kevin Leyton-Brown. 2009. SATzilla2009: an automatic algorithm portfolio for SAT. (2009)."},{"key":"e_1_3_2_2_48_1","volume-title":"Proceedings of the 32nd International Conference on Neural Information Processing Systems.","author":"Yolcu Emre","year":"2019","unstructured":"Emre Yolcu and Barnab\u00e1s P\u00f3czos. 2019. Learning Local Search Heuristics for Boolean Satisfiability. In Proceedings of the 32nd International Conference on Neural Information Processing Systems."},{"key":"e_1_3_2_2_49_1","volume-title":"Proceedings of the 32th International Conference on Neural Information Processing Systems.","author":"You Jiaxuan","year":"2019","unstructured":"Jiaxuan You, Haoze Wu, Clark Barrett, Raghuram Ramanujan, and Jure Leskovec. 2019. G2SAT: Learning to Generate SAT Formulas. In Proceedings of the 32th International Conference on Neural Information Processing Systems."},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3292500.3330961"}],"event":{"name":"KDD '24: The 30th ACM SIGKDD Conference on Knowledge Discovery and Data Mining","location":"Barcelona Spain","acronym":"KDD '24","sponsor":["SIGMOD ACM Special Interest Group on Management of Data","SIGKDD ACM Special Interest Group on Knowledge Discovery in Data"]},"container-title":["Proceedings of the 30th ACM SIGKDD Conference on Knowledge Discovery and Data Mining"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3637528.3671627","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3637528.3671627","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:05:59Z","timestamp":1750291559000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3637528.3671627"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,24]]},"references-count":50,"alternative-id":["10.1145\/3637528.3671627","10.1145\/3637528"],"URL":"https:\/\/doi.org\/10.1145\/3637528.3671627","relation":{},"subject":[],"published":{"date-parts":[[2024,8,24]]},"assertion":[{"value":"2024-08-24","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}