{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T04:21:30Z","timestamp":1780633290803,"version":"3.54.1"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030242572","type":"print"},{"value":"9783030242589","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-24258-9_24","type":"book-chapter","created":{"date-parts":[[2019,6,28]],"date-time":"2019-06-28T21:02:31Z","timestamp":1561755751000},"page":"336-353","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":48,"title":["Guiding High-Performance SAT Solvers with Unsat-Core Predictions"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Selsam","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nikolaj","family":"Bj\u00f8rner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,6,29]]},"reference":[{"key":"24_CR1","unstructured":"Abadi, M., et al.: TensorFlow: a system for large-scale machine learning. In: 12th USENIX Symposium on Operating Systems Design and Implementation OSDI 16, pp. 265\u2013283 (2016)"},{"key":"24_CR2","unstructured":"Balcan, M., Dick, T., Sandholm, T., Vitercik, E.: Learning to branch. In: Dy, J.G., Krause, A. (eds.) Proceedings of the 35th International Conference on Machine Learning, ICML 2018, Stockholmsm\u00e4ssan, Stockholm, Sweden, July 10\u201315, 2018. JMLR Workshop and Conference Proceedings, vol. 80, pp. 353\u2013362. JMLR.org (2018). http:\/\/proceedings.mlr.press\/v80\/balcan18a.html"},{"key":"24_CR3","unstructured":"Balunovic, M., Bielik, P., Vechev, M.T.: Learning to solve SMT formulas. In: Bengio, S., Wallach, H.M., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, 3\u20138 December 2018, Montr\u00e9al, Canada. pp. 10338\u201310349 (2018). http:\/\/papers.nips.cc\/paper\/8233-learning-to-solve-smt-formulas"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/978-3-319-24318-4_29","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"A Biere","year":"2015","unstructured":"Biere, A., Fr\u00f6hlich, A.: Evaluating CDCL variable scoring schemes. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 405\u2013422. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_29"},{"key":"24_CR5","volume-title":"Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)"},{"key":"24_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-642-36675-8_2","volume-title":"Automated Reasoning and Mathematics","author":"L Moura de","year":"2013","unstructured":"de Moura, L., Passmore, G.O.: The Strategy Challenge in SMT Solving. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS (LNAI), vol. 7788, pp. 15\u201344. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36675-8_2"},{"key":"24_CR7","unstructured":"Devlin, J., Uesato, J., Bhupatiraju, S., Singh, R., Mohamed, A.r., Kohli, P.: RobustFill: neural program learning under noisy I\/O. In: Proceedings of the 34th International Conference on Machine Learning, vol. 70, pp. 990\u2013998. JMLR. org (2017)"},{"key":"24_CR8","doi-asserted-by":"publisher","unstructured":"Heule, M., van Maaren, H.: Look-ahead based SAT solvers. In: Biere et al. [5], pp. 155\u2013184. https:\/\/doi.org\/10.3233\/978-1-58603-929-5-155","DOI":"10.3233\/978-1-58603-929-5-155"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Heule, M.J.: Schur number five. In: Thirty-Second AAAI Conference on Artificial Intelligence (2018)","DOI":"10.1609\/aaai.v32i1.12209"},{"key":"24_CR10","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-319-63516-3_2","volume-title":"Handbook of Parallel Constraint Reasoning","author":"MJH Heule","year":"2018","unstructured":"Heule, M.J.H., Kullmann, O., Biere, A.: Cube-and-conquer for satisfiability. Handbook of Parallel Constraint Reasoning, pp. 31\u201359. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-63516-3_2"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-319-40970-2_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"MJH Heule","year":"2016","unstructured":"Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 228\u2013245. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_15"},{"key":"24_CR12","unstructured":"Proceedings of sat competition 2018; solver and benchmark descriptions (2018). http:\/\/hdl.handle.net\/10138\/237063"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"Hinton, G., et al.: Deep neural networks for acoustic modeling in speech recognition. IEEE Sig. Process. Mag. 29 (2012)","DOI":"10.1109\/MSP.2012.2205597"},{"issue":"8","key":"24_CR14","doi-asserted-by":"publisher","first-page":"1735","DOI":"10.1162\/neco.1997.9.8.1735","volume":"9","author":"S Hochreiter","year":"1997","unstructured":"Hochreiter, S., Schmidhuber, J.: Long short-term memory. Neural Comput. 9(8), 1735\u20131780 (1997)","journal-title":"Neural Comput."},{"key":"24_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-319-40229-1_22","volume-title":"Automated Reasoning","author":"K Hoder","year":"2016","unstructured":"Hoder, K., Reger, G., Suda, M., Voronkov, A.: Selecting the selection. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 313\u2013329. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_22"},{"key":"24_CR16","unstructured":"Huang, D., Dhariwal, P., Song, D., Sutskever, I.: GamePad: A learning environment for theorem proving. arXiv preprint arXiv:1806.00608 (2018)"},{"key":"24_CR17","unstructured":"Irving, G., Szegedy, C., Alemi, A.A., Een, N., Chollet, F., Urban, J.: DeepMath-deep sequence models for premise selection. In: Advances in Neural Information Processing Systems, pp. 2235\u20132243 (2016)"},{"key":"24_CR18","unstructured":"Kaliszyk, C., Chollet, F., Szegedy, C.: HolStep: A machine learning dataset for higher-order logic theorem proving. arXiv preprint arXiv:1703.00426 (2017)"},{"key":"24_CR19","unstructured":"Kingma, D.P., Ba, J.: Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980 (2014)"},{"issue":"129","key":"24_CR20","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1090\/S0025-5718-1975-0373371-6","volume":"29","author":"DE Knuth","year":"1975","unstructured":"Knuth, D.E.: Estimating the efficiency of backtrack programs. Math. Comput. 29(129), 122\u2013136 (1975)","journal-title":"Math. Comput."},{"key":"24_CR21","unstructured":"Knuth, D.E.: The Art of Computer Programming, vol. 4, Fascicle 6: Satisfiability (2015)"},{"key":"24_CR22","unstructured":"Krizhevsky, A., Sutskever, I., Hinton, G.E.: ImageNet classification with deep convolutional neural networks. In: Advances in neural information processing systems, pp. 1097\u20131105 (2012)"},{"issue":"1","key":"24_CR23","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1214\/aoms\/1177729694","volume":"22","author":"S Kullback","year":"1951","unstructured":"Kullback, S., Leibler, R.A.: On information and sufficiency. Ann. Math. Stat. 22(1), 79\u201386 (1951)","journal-title":"Ann. Math. Stat."},{"key":"24_CR24","doi-asserted-by":"publisher","unstructured":"Kullmann, O.: Fundaments of branching heuristics. In: Biere et al. [5], pp. 205\u2013244. https:\/\/doi.org\/10.3233\/978-1-58603-929-5-205","DOI":"10.3233\/978-1-58603-929-5-205"},{"issue":"4","key":"24_CR25","doi-asserted-by":"publisher","first-page":"699","DOI":"10.1287\/opre.14.4.699","volume":"14","author":"EL Lawler","year":"1966","unstructured":"Lawler, E.L., Wood, D.E.: Branch-and-bound methods: a survey. Oper. Res. 14(4), 699\u2013719 (1966)","journal-title":"Oper. Res."},{"key":"24_CR26","doi-asserted-by":"publisher","unstructured":"Liang, J., K., H.G.V., Poupart, P., Czarnecki, K., Ganesh, V.: An empirical study of branching heuristics through the lens of global learning rate. In: Lang, J. (ed.) Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, 13\u201319 July 2018, Stockholm, Sweden, pp. 5319\u20135323. ijcai.org (2018). https:\/\/doi.org\/10.24963\/ijcai.2018\/745 , http:\/\/www.ijcai.org\/proceedings\/2018\/","DOI":"10.24963\/ijcai.2018\/745"},{"key":"24_CR27","unstructured":"Loos, S.M., Irving, G., Szegedy, C., Kaliszyk, C.: Deep network guided proof search. In: Eiter, T., Sands, D. (eds.) LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7\u201312, 2017. EPiC Series in Computing, vol. 46, pp. 85\u2013105. EasyChair (2017). http:\/\/www.easychair.org\/publications\/paper\/340345"},{"issue":"5","key":"24_CR28","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JP Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Transact. Comput. 48(5), 506\u2013521 (1999)","journal-title":"IEEE Transact. Comput."},{"key":"24_CR29","unstructured":"Mijnders, S., de Wilde, B., Heule, M.: Symbiosis of search and heuristics for random 3-sat. CoRR abs\/1402.4455 (2010)"},{"key":"24_CR30","unstructured":"Moritz, P., et al.: Ray: a distributed framework for emerging $$\\{$$ AI $$\\}$$ applications. In: 13th USENIX Symposium on Operating Systems Design and Implementation OSDI 18), pp. 561\u2013577 (2018)"},{"key":"24_CR31","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient sat solver. In: Proceedings of the 38th annual Design Automation Conference. pp. 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"key":"24_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-319-24318-4_23","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"C Oh","year":"2015","unstructured":"Oh, C.: Between SAT and UNSAT: The fundamental difference in CDCL SAT. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 307\u2013323. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_23"},{"key":"24_CR33","unstructured":"Parisotto, E., Mohamed, A.r., Singh, R., Li, L., Zhou, D., Kohli, P.: Neuro-symbolic program synthesis. arXiv preprint arXiv:1611.01855 (2016)"},{"key":"24_CR34","unstructured":"Ryan, L.: Efficient algorithms for clause-learning SAT solvers, Masters thesis (2004)"},{"issue":"2, 3","key":"24_CR35","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E-A brainiac theorem prover. Ai Communicat. 15(2, 3), 111\u2013126 (2002)","journal-title":"Ai Communicat."},{"key":"24_CR36","unstructured":"Schulz, S.: We know (nearly) nothing! but can we learn? In: Reger, G., Traytel, D. (eds.) ARCADE 2017, 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, Gothenburg, Sweden, 6th August 2017. EPiC Series in Computing, vol. 51, pp. 29\u201332. EasyChair (2017). http:\/\/www.easychair.org\/publications\/paper\/6kgF"},{"key":"24_CR37","unstructured":"Selsam, D., Lamm, M., B\u00fcnz, B., Liang, P., de Moura, L., Dill, D.L.: Learning a SAT solver from single-bit supervision. In: International Conference on Learning Representations (2019). https:\/\/openreview.net\/forum?id=HJMC_iA5tm"},{"issue":"7676","key":"24_CR38","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1038\/nature24270","volume":"550","author":"D Silver","year":"2017","unstructured":"Silver, D., et al.: Mastering the game of go without human knowledge. Nature 550(7676), 354\u2013359 (2017)","journal-title":"Nature"},{"issue":"2","key":"24_CR39","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)","journal-title":"AI Mag."},{"issue":"2","key":"24_CR40","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":"24_CR41","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-540-71070-7_37","volume-title":"Automated Reasoning","author":"J Urban","year":"2008","unstructured":"Urban, J., Sutcliffe, G., Pudl\u00e1k, P., Vysko\u010dil, J.: MaLARea SG1 - Machine learner for automated reasoning with semantic guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 441\u2013456. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_37"},{"key":"24_CR42","unstructured":"Wang, M., Tang, Y., Wang, J., Deng, J.: Premise selection for theorem proving by deep graph embedding. In: Advances in Neural Information Processing Systems, pp. 2786\u20132796 (2017)"},{"key":"24_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-319-09284-3_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"N Wetzler","year":"2014","unstructured":"Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422\u2013429. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_31"},{"key":"24_CR44","unstructured":"Whalen, D.: Holophrasm: a neural automated theorem prover for higher-order logic. arXiv preprint arXiv:1608.02644 (2016)"},{"key":"24_CR45","unstructured":"Wu, Y., et al.: Google\u2019s neural machine translation system: Bridging the gap between human and machine translation. arXiv preprint arXiv:1609.08144 (2016)"},{"key":"24_CR46","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1613\/jair.2490","volume":"32","author":"L Xu","year":"2008","unstructured":"Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: Satzilla: Portfolio-based algorithm selection for SAT. J. Artif. Intell. Res. 32, 565\u2013606 (2008). https:\/\/doi.org\/10.1613\/jair.2490","journal-title":"J. Artif. Intell. Res."}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2019"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-24258-9_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,22]],"date-time":"2022-09-22T10:34:52Z","timestamp":1663842892000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-24258-9_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030242572","9783030242589"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-24258-9_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"29 June 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Theory and Applications of Satisfiability Testing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sat2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/sat2019.tecnico.ulisboa.pt\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"64","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}