{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T12:53:06Z","timestamp":1760014386014,"version":"3.40.5"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031634970"},{"type":"electronic","value":"9783031634987"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T00:00:00Z","timestamp":1719792000000},"content-version":"vor","delay-in-days":182,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>To achieve the best performance, automatic theorem provers often rely on schedules of diverse proving strategies to be tried out (either sequentially or in parallel) on a given problem. In this paper, we report on a large-scale experiment with discovering strategies for the Vampire prover, targeting the FOF fragment of the TPTP library and constructing a schedule for it, based on the ideas of Andrei Voronkov\u2019s system Spider. We examine the process from various angles, discuss the difficulty (or ease) of obtaining a strong Vampire schedule for the CASC competition, and establish how well a schedule can be expected to generalize to unseen problems and what factors influence this property.<\/jats:p>","DOI":"10.1007\/978-3-031-63498-7_12","type":"book-chapter","created":{"date-parts":[[2024,6,30]],"date-time":"2024-06-30T19:01:44Z","timestamp":1719774104000},"page":"194-213","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Regularization in\u00a0Spider-Style Strategy Discovery and\u00a0Schedule Construction"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1822-2651","authenticated-orcid":false,"given":"Filip","family":"B\u00e1rtek","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0541-3889","authenticated-orcid":false,"given":"Karel","family":"Chvalovsk\u00fd","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0989-5800","authenticated-orcid":false,"given":"Martin","family":"Suda","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,1]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","unstructured":"B\u00e1rtek, F., Chvalovsk\u00fd, K., Suda, M.: Regularization in spider-style strategy discovery and schedule construction (2024). https:\/\/doi.org\/10.48550\/arXiv.2403.12869","DOI":"10.48550\/arXiv.2403.12869"},{"key":"12_CR2","doi-asserted-by":"publisher","unstructured":"B\u00e1rtek, F., Suda, M.: Vampire strategy performance measurements (2024). https:\/\/doi.org\/10.5281\/zenodo.10814478","DOI":"10.5281\/zenodo.10814478"},{"issue":"3","key":"12_CR3","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1287\/moor.4.3.233","volume":"4","author":"V Chv\u00e1tal","year":"1979","unstructured":"Chv\u00e1tal, V.: A greedy heuristic for the set-covering problem. Math. Oper. Res. 4(3), 233\u2013235 (1979). https:\/\/doi.org\/10.1287\/moor.4.3.233","journal-title":"Math. Oper. Res."},{"key":"12_CR4","unstructured":"Gottlob, G., Sutcliffe, G., Voronkov, A. (eds.): Global Conference on Artificial Intelligence, GCAI 2015, Tbilis, 16\u201319 October 2015, EPiC Series in Computing, vol.\u00a036. EasyChair (2015). https:\/\/easychair.org\/publications\/volume\/GCAI_2015"},{"key":"12_CR5","unstructured":"Gurobi Optimization, LLC. Gurobi Optimizer Reference Manual (2023). https:\/\/www.gurobi.com"},{"key":"12_CR6","doi-asserted-by":"publisher","unstructured":"Hastie, T., Tibshirani, R., Friedman, J.: The Elements of Statistical Learning, 2nd edn. SSS, Springer, New York (2009). https:\/\/doi.org\/10.1007\/978-0-387-84858-7","DOI":"10.1007\/978-0-387-84858-7"},{"key":"12_CR7","doi-asserted-by":"publisher","unstructured":"Holden, E.K., Korovin, K.: Heterogeneous heuristic optimisation and scheduling for first-order theorem proving. In: Kamareddine, F., Coen, C.S. (eds.) CICM 2021. LNCS, vol. 12833, pp. 107\u2013123. Springer, Cham (2021).https:\/\/doi.org\/10.1007\/978-3-030-81097-9_8","DOI":"10.1007\/978-3-030-81097-9_8"},{"key":"12_CR8","doi-asserted-by":"publisher","unstructured":"Hutter, F., Hoos, H.H., Leyton-Brown, K., St\u00fctzle, T.: ParamILS: an automatic algorithm configuration framework. J. Artif. Intell. Res. 36, 267\u2013306 (2009). https:\/\/doi.org\/10.1613\/JAIR.2861","DOI":"10.1613\/JAIR.2861"},{"key":"12_CR9","doi-asserted-by":"publisher","unstructured":"Hula, J., Jakubuv, J., Janota, M., Kubej, L.: Targeted configuration of an SMT solver. In: Buzzard, K., Kutsia, T. (eds.) CICM 2022. LNCS, vol. 13467, pp. 256\u2013271. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-16681-5_18","DOI":"10.1007\/978-3-031-16681-5_18"},{"key":"12_CR10","doi-asserted-by":"publisher","unstructured":"Jakubuv, J., et al.: MizAR 60 for Mizar 50. In: Naumowicz, A., Thiemann, R. (eds.) 14th International Conference on Interactive Theorem Proving, ITP 2023, 31 July to 4 August 2023, Bia\u0142ystok. LIPIcs, vol.\u00a0268, pp. 19:1\u201319:22. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2023.19","DOI":"10.4230\/LIPICS.ITP.2023.19"},{"key":"12_CR11","doi-asserted-by":"publisher","unstructured":"Jakubuv, J., Suda, M., Urban, J.: Automated invention of strategies and term orderings for Vampire. In: Benzm\u00fcller, C., Lisetti, C.L., Theobald, M. (eds.) GCAI 2017, 3rd Global Conference on Artificial Intelligence, Miami, 18\u201322 October 2017. EPiC Series in Computing, vol.\u00a050, pp. 121\u2013133. EasyChair (2017). https:\/\/doi.org\/10.29007\/XGHJ","DOI":"10.29007\/XGHJ"},{"key":"12_CR12","doi-asserted-by":"publisher","unstructured":"Jakubuv, J., Urban, J.: BliStrTune: hierarchical invention of theorem proving strategies. In: Bertot, Y., Vafeiadis, V. (eds.) Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, 16\u201317 January 2017, pp. 43\u201352. ACM (2017).https:\/\/doi.org\/10.1145\/3018610.3018619","DOI":"10.1145\/3018610.3018619"},{"issue":"1","key":"12_CR13","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/S0020-0190(99)00031-9","volume":"70","author":"S Khuller","year":"1999","unstructured":"Khuller, S., Moss, A., Naor, J.: The budgeted maximum coverage problem. Inf. Process. Lett. 70(1), 39\u201345 (1999). https:\/\/doi.org\/10.1016\/S0020-0190(99)00031-9","journal-title":"Inf. Process. Lett."},{"key":"12_CR14","doi-asserted-by":"publisher","unstructured":"Korovin, K.: iProver\u2014an instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 292\u2013298. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_24","DOI":"10.1007\/978-3-540-71070-7_24"},{"key":"12_CR15","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1","DOI":"10.1007\/978-3-642-39799-8_1"},{"issue":"2","key":"12_CR16","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/s10817-015-9329-1","volume":"55","author":"D K\u00fchlwein","year":"2015","unstructured":"K\u00fchlwein, D., Urban, J.: MaLeS: a framework for automatic tuning of automated theorem provers. J. Autom. Reason. 55(2), 91\u2013116 (2015). https:\/\/doi.org\/10.1007\/s10817-015-9329-1","journal-title":"J. Autom. Reason."},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Lindauer, M., et al.: SMAC3: a versatile bayesian optimization package for hyperparameter optimization. J. Mach. Learn. Res. 23, 54:1\u201354:9 (2022). http:\/\/jmlr.org\/papers\/v23\/21-0888.html","DOI":"10.1055\/a-1666-1719"},{"issue":"4","key":"12_CR18","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/0020-0190(93)90029-9","volume":"47","author":"M Luby","year":"1993","unstructured":"Luby, M., Sinclair, A., Zuckerman, D.: Optimal speedup of Las Vegas algorithms. Inf. Process. Lett. 47(4), 173\u2013180 (1993). https:\/\/doi.org\/10.1016\/0020-0190(93)90029-9","journal-title":"Inf. Process. Lett."},{"key":"12_CR19","doi-asserted-by":"publisher","unstructured":"Mangla, C., Holden, S.B., Paulson, L.C.: Bayesian ranking for strategy scheduling in automated theorem provers. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) IJCAR 2022. LNCS, vol. 13385, pp. 559\u2013577. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_33","DOI":"10.1007\/978-3-031-10769-6_33"},{"key":"12_CR20","doi-asserted-by":"publisher","unstructured":"Reger, G., Suda, M., Voronkov, A.: New techniques in clausal form generation. In: Benzm\u00fcller, C., Sutcliffe, G., Rojas, R. (eds.) GCAI 2016. 2nd Global Conference on Artificial Intelligence, 19 September\u20132 October 2016, Berlin. EPiC Series in Computing, vol.\u00a041, pp. 11\u201323. EasyChair (2016). https:\/\/doi.org\/10.29007\/DZFZ","DOI":"10.29007\/DZFZ"},{"key":"12_CR21","doi-asserted-by":"publisher","unstructured":"Sch\u00e4fer, S., Schulz, S.: Breeding theorem proving heuristics with genetic algorithms. In: Gottlob et\u00a0al. [4], pp. 263\u2013274. https:\/\/doi.org\/10.29007\/gms9","DOI":"10.29007\/gms9"},{"key":"12_CR22","doi-asserted-by":"publisher","unstructured":"Schede, E., et al.: A survey of methods for automated algorithm configuration. J. Artif. Intell. Res. 75, 425\u2013487 (2022). https:\/\/doi.org\/10.1613\/jair.1.13676","DOI":"10.1613\/jair.1.13676"},{"key":"12_CR23","doi-asserted-by":"publisher","unstructured":"Schulz, S., Cruanes, S., Vukmirovi\u0107, P.: Faster, higher, stronger: E 2.3. In: Fontaine, P. (ed.) CADE 27. LNCS, vol. 11716, pp. 495\u2013507. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_29","DOI":"10.1007\/978-3-030-29436-6_29"},{"key":"12_CR24","unstructured":"Schurr, H.: Optimal strategy schedules for everyone. In: Konev, B., Schon, C., Steen, A. (eds.) Proceedings of the Workshop on Practical Aspects of Automated Reasoning Co-located with the 11th International Joint Conference on Automated Reasoning (FLoC\/IJCAR 2022), Haifa, 11\u201312 August 2022. CEUR Workshop Proceedings, vol.\u00a03201. CEUR-WS.org (2022). https:\/\/ceur-ws.org\/Vol-3201\/paper8.pdf"},{"key":"12_CR25","doi-asserted-by":"publisher","unstructured":"Seipp, J., Sievers, S., Helmert, M., Hutter, F.: Automatic configuration of sequential planning portfolios. In: Bonet, B., Koenig, S. (eds.) Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, 25\u201330 January 2015, Austin, pp. 3364\u20133370. AAAI Press (2015). https:\/\/doi.org\/10.1609\/AAAI.V29I1.9640","DOI":"10.1609\/AAAI.V29I1.9640"},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"Suda, M.: Vampire getting noisy: will random bits help conquer chaos? (system description). EasyChair Preprint no. 7719 (2022). https:\/\/easychair.org\/publications\/preprint\/CSVF","DOI":"10.1007\/978-3-031-10769-6_38"},{"issue":"2","key":"12_CR27","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1609\/AIMAG.V37I2.2620","volume":"37","author":"G Sutcliffe","year":"2016","unstructured":"Sutcliffe, G.: The CADE ATP system competition - CASC. AI Mag. 37(2), 99\u2013101 (2016). https:\/\/doi.org\/10.1609\/AIMAG.V37I2.2620","journal-title":"AI Mag."},{"key":"12_CR28","doi-asserted-by":"publisher","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure: from CNF to TH0, TPTP v6.4.0. J. Automat. Reason. 59(4), 483\u2013502 (2017). https:\/\/doi.org\/10.1007\/s10817-017-9407-7","DOI":"10.1007\/s10817-017-9407-7"},{"issue":"1","key":"12_CR29","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1023\/A:1006006930186","volume":"21","author":"CB Suttner","year":"1998","unstructured":"Suttner, C.B., Sutcliffe, G.: The CADE-14 ATP system competition. J. Autom. Reason. 21(1), 99\u2013134 (1998). https:\/\/doi.org\/10.1023\/A:1006006930186","journal-title":"J. Autom. Reason."},{"issue":"2","key":"12_CR30","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1023\/A:1005887414560","volume":"18","author":"T Tammet","year":"1997","unstructured":"Tammet, T.: Gandalf. J. Autom. Reason. 18(2), 199\u2013204 (1997). https:\/\/doi.org\/10.1023\/A:1005887414560","journal-title":"J. Autom. Reason."},{"key":"12_CR31","unstructured":"Tammet, T.: Gandalf c-1.1 (1998). https:\/\/www.tptp.org\/CASC\/15\/SystemDescriptions.html#Gandalf. Accessed 25 Jan 2023"},{"key":"12_CR32","doi-asserted-by":"publisher","unstructured":"Tammet, T.: Towards efficient subsumption. In: Kirchner, C., Kirchner, H. (eds.) CADE-15. LNCS, vol.\u00a01421, pp. 427\u2013441. Springer, Cham (1998). https:\/\/doi.org\/10.1007\/BFb0054276","DOI":"10.1007\/BFb0054276"},{"key":"12_CR33","doi-asserted-by":"publisher","unstructured":"Urban, J.: BliStr: The blind strategymaker. In: Gottlob et\u00a0al. [4], pp. 312\u2013331. https:\/\/doi.org\/10.29007\/8n7m","DOI":"10.29007\/8n7m"},{"key":"12_CR34","unstructured":"Voronkov, A.: Spider: learning in the sea of options (2023). https:\/\/easychair.org\/smart-program\/Vampire23\/2023-07-05.html#talk:223833. Unpublished. Paper accepted at Vampire23: The 7th Vampire Workshop"},{"key":"12_CR35","unstructured":"Wolf, A., Letz, R.: Strategy parallelism in automated theorem proving. In: Cook, D.J. (ed.) Proceedings of the Eleventh International Florida Artificial Intelligence Research Society Conference, 18\u201320 May 1998, Sanibel Island, pp. 142\u2013146. AAAI Press (1998). http:\/\/www.aaai.org\/Library\/FLAIRS\/1998\/flairs98-027.php"},{"key":"12_CR36","unstructured":"Xu, L., Hoos, H.H., Leyton-Brown, K.: Hydra: automatically configuring algorithms for portfolio-based selection. In: Fox, M., Poole, D. (eds.) Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2010, Atlanta, 11\u201315 July 2010. AAAI Press (2010). http:\/\/www.aaai.org\/ocs\/index.php\/AAAI\/AAAI10\/paper\/view\/1929"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-63498-7_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:17:18Z","timestamp":1747592238000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63498-7_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031634970","9783031634987"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63498-7_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"1 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nancy","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/merz.gitlabpages.inria.fr\/2024-ijcar\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}