{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,28]],"date-time":"2026-09-28T16:13:11Z","timestamp":1790611991268,"version":"4.1.0"},"reference-count":96,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2022,6,1]],"date-time":"2022-06-01T00:00:00Z","timestamp":1654041600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,6,1]],"date-time":"2022-06-01T00:00:00Z","timestamp":1654041600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2022,6]]},"DOI":"10.1007\/s10703-023-00430-1","type":"journal-article","created":{"date-parts":[[2023,6,14]],"date-time":"2023-06-14T11:02:11Z","timestamp":1686740531000},"page":"426-451","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Machine learning and logic: a new frontier in artificial intelligence"],"prefix":"10.1007","volume":"60","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6029-2047","authenticated-orcid":false,"given":"Vijay","family":"Ganesh","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Somesh","family":"Jha","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,6,14]]},"reference":[{"key":"430_CR1","doi-asserted-by":"crossref","unstructured":"Alur R, Bodik R, Juniwal G, Martin Milo MK, Raghothaman M, Seshia SA, Singh R, Solar-Lezama A, Torlak E, Udupa A (2013) Syntax-guided synthesis. In: Proceedings of the IEEE international conference on formal methods in computer-aided design (FMCAD), pp 1\u201317","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"430_CR2","doi-asserted-by":"crossref","unstructured":"Abate A, David C, Kesseli P, Kroening D, Polgreen E (2018) Counterexample guided inductive synthesis modulo theories. In: Computer aided verification-30th international conference (CAV), volume 10981 of Lecture Notes in Computer Science, pp 270\u2013288. Springer","DOI":"10.1007\/978-3-319-96145-3_15"},{"key":"430_CR3","first-page":"114","volume-title":"Theory and Applications of Satisfiability Testing - SAT","author":"A Atserias","year":"2009","unstructured":"Atserias A, Fichte JK, Thurley M (2009) Clause-learning algorithms with many restarts and bounded-width resolution. In: Kullmann O (ed) Theory and Applications of Satisfiability Testing - SAT. Springer, Berlin Heidelberg, Berlin, Heidelberg, pp 114\u2013127"},{"issue":"4","key":"430_CR4","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00116828","volume":"2","author":"D Angluin","year":"1988","unstructured":"Angluin D (1988) Queries and concept learning. Mach Learn 2(4):319\u2013342","journal-title":"Mach Learn"},{"key":"430_CR5","unstructured":"Audemard Gilles, Simon Laurent (2013) Glucose 2.3 in the SAT 2013 Competition. In: Proceedings of SAT competition 2013, pp 42\u201343"},{"issue":"12","key":"430_CR6","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1145\/3208071","volume":"61","author":"R Alur","year":"2018","unstructured":"Alur R, Singh R, Fisman D, Solar-Lezama A (2018) Search-based program synthesis. Commun ACM 61(12):84\u201393","journal-title":"Commun ACM"},{"key":"430_CR7","doi-asserted-by":"crossref","unstructured":"Ashok D, Scott J, Wetzel SJ, Panju M, Ganesh V (2021) Logic guided genetic algorithms. In: 35th AAAI conference on artificial intelligence, AAAI 2021, 33rd Conference on innovative applications of artificial intelligence, IAAI 2021, The 11th symposium on educational advances in artificial intelligence, EAAI 2021, virtual event, Feb 2\u20139, 2021, pp 15753\u201315754. AAAI Press","DOI":"10.1609\/aaai.v35i18.17873"},{"key":"430_CR8","unstructured":"Alaa AM, Schaar M van\u00a0der (2019) Demystifying black-box models with symbolic metamodels. Adv Neural Inf Process Syst 32"},{"key":"430_CR9","unstructured":"Bouraoui Z, Cornu\u00e9jols A, Denoeux T, Destercke S, Dubois D, Guillaume R, Marques-Silva J, Mengin J, Prade H, Schockaert S, Serrurier M, Vrain C (2019) From shallow to deep interactions between knowledge representation, reasoning and machine learning (kay r. amel group). CoRR, abs\/1912.06612"},{"key":"430_CR10","unstructured":"Biere A, Heule M, van Maaren H, Walsh T (2009) (eds) Handbook of Satisfiability, vol. 185 of Frontiers in Artificial Intelligence and Applications. IOS Press"},{"key":"430_CR11","unstructured":"B\u00fcnz B, Lamm M (2017) Graph neural networks and boolean satisfiability. CoRR, abs\/1702.03592"},{"issue":"7","key":"430_CR12","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/3448250","volume":"64","author":"Y Bengio","year":"2021","unstructured":"Bengio Y, LeCun Y, Hinton GE (2021) Deep learning for AI. Commun ACM 64(7):58\u201365","journal-title":"Commun ACM"},{"key":"430_CR13","unstructured":"Bak S, Liu C, Johnson TT (2021) The second international verification of neural networks competition (VNN-COMP 2021): Summary and results. CoRR, abs\/2109.00498"},{"issue":"7","key":"430_CR14","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/1965724.1965743","volume":"54","author":"T Ball","year":"2011","unstructured":"Ball T, Levin V, Rajamani SK (2011) A decade of software model checking with SLAM. Commun ACM 54(7):68\u201376","journal-title":"Commun ACM"},{"key":"430_CR15","unstructured":"Bansal K, Loos SM, Rabe MN, Szegedy C, Wilcox S (2019) Holist: an environment for machine learning of higher order logic theorem proving. In: Kamalika C and Ruslan S, (eds.) Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, volume\u00a097 of Proceedings of Machine Learning Research, pp 454\u2013463. PMLR"},{"key":"430_CR16","doi-asserted-by":"crossref","unstructured":"Bader-El-Den MB, Poli R (2007) Generating SAT local-search heuristics using a GP hyper-heuristic framework. In: Nicolas M, El-Ghazali T, Pierre C, Marc S, Evelyne L, (eds), Artificial Evolution, 8th International Conference, Evolution Artificielle, EA 2007, Tours, France, October 29-31, 2007, revised selected papers, volume 4926 of Lecture Notes in Computer Science, Springer, pp 37\u201349","DOI":"10.1007\/978-3-540-79305-2_4"},{"issue":"1","key":"430_CR17","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E Clarke","year":"2001","unstructured":"Clarke E, Biere A, Raimi R, Zhu Y (2001) Bounded model checking using satisfiability solving. Formal Methods Syst Des 19(1):7\u201334","journal-title":"Formal Methods Syst Des"},{"issue":"1","key":"430_CR18","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/s10994-021-06089-1","volume":"111","author":"A Cropper","year":"2022","unstructured":"Cropper A, Dumancic S, Evans R, Muggleton SH (2022) Inductive logic programming at 30. Mach Learn 111(1):147\u2013172","journal-title":"Mach Learn"},{"key":"430_CR19","doi-asserted-by":"crossref","unstructured":"Clarke EM, Emerson EA (1981) Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of programs, pp 52\u201371","DOI":"10.1007\/BFb0025774"},{"key":"430_CR20","doi-asserted-by":"crossref","unstructured":"Clarke EM, Fehnker A, Han Z, Krogh BH, Stursberg O, Theobald M (2003) Verification of hybrid systems based on counterexample-guided abstraction refinement. In: TACAS, pp 192\u2013207","DOI":"10.1007\/3-540-36577-X_14"},{"key":"430_CR21","doi-asserted-by":"crossref","unstructured":"Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: 12th international conference on computer aided verification (CAV), vol. 1855 of Lecture Notes in Computer Science, Springer, pp 154\u2013169","DOI":"10.1007\/10722167_15"},{"issue":"5","key":"430_CR22","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke EM, Grumberg O, Jha S, Yuan L, Veith H (2003) Counterexample-guided abstraction refinement for symbolic model checking. J ACM 50(5):752\u2013794","journal-title":"J ACM"},{"key":"430_CR23","doi-asserted-by":"crossref","unstructured":"Clarke EM, Gupta A, Kukula JH, Strichman O (2002) SAT based abstraction-refinement using ILP and machine learning techniques. In: computer aided verification, 14th international conference (CAV), vol. 2404 of Lecture Notes in Computer Science, Springer, pp 265\u2013279","DOI":"10.1007\/3-540-45657-0_20"},{"key":"430_CR24","doi-asserted-by":"crossref","unstructured":"Cadar C, Ganesh V, Pawlowski PM, Dill DL, Engler DR (2006) EXE: automatically generating inputs of death. In: Proceedings of the 13th ACM conference on computer and communications security, CCS \u201906, New York, NY, USA. ACM, pp 322\u2013335","DOI":"10.1145\/1180405.1180445"},{"key":"430_CR25","doi-asserted-by":"crossref","unstructured":"Cook S (1971) The complexity of theorem-proving procedures. In: proceedings of the third annual ACM symposium on theory of computing (STOC), ACM, pp 151\u2013158","DOI":"10.1145\/800157.805047"},{"key":"430_CR26","unstructured":"Dash T, Chitlangia S, Ahuja A, Srinivasan A (2021) How to tell deep neural networks what we know. CoRR, abs\/2107.10295"},{"issue":"7","key":"430_CR27","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis M, Logemann G, Loveland D (1962) A machine program for theorem-proving. Commun ACM 5(7):394\u2013397","journal-title":"Commun ACM"},{"key":"430_CR28","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura L, Bj\u00f8rner N (2008) Z3: An efficient smt solver. In: international conference on tools and algorithms for the construction and analysis of systems, Springer, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"430_CR29","unstructured":"Duan H, Nejati S, Trimponias G, Poupart P, Ganesh V (2020) Online bayesian moment matching based SAT solver heuristics. In: Proceedings of the 37th international conference on machine learning, ICML 2020, 13\u201318 July 2020, Virtual Event, vol. 119 of proceedings of machine learning research, PMLR, pp 2710\u20132719"},{"key":"430_CR30","unstructured":"Devlin D, O\u2019Sullivan B (2008) Satisfiability as a classification problem. In: Proceedings of the 19th Irish Conference on artificial intelligence and cognitive science"},{"key":"430_CR31","doi-asserted-by":"crossref","unstructured":"Dubois D, Prade H (2019) Towards a reconciliation between reasoning and learning-a position paper. In: Nahla\u00a0Ben A, Benjamin Q, Martin T, (eds) scalable uncertainty management-13th international conference, SUM 2019, Compi\u00e8gne, France, Dec 16\u201318, 2019, Proceedings, vol. 11940 of lecture notes in computer science, Springer, pp 153\u2013168","DOI":"10.1007\/978-3-030-35514-2_12"},{"key":"430_CR32","doi-asserted-by":"crossref","unstructured":"E\u00e9n N, S\u00f6rensson N (2004) Theory and applications of satisfiability testing: 6th international conference, SAT 2003, santa margherita ligure, Italy, May 5\u20138, 2003, selected revised papers, chapter an extensible SAT-solver, Springer Berlin Heidelberg, Berlin, Heidelberg, pp 502\u2013518","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"430_CR33","doi-asserted-by":"crossref","unstructured":"Ertel W, Schumann J, Suttner CB (1989) Learning heuristics for a theorem prover using back propagation. In: Johannes R, Karl L, (eds) 5. \u00d6sterreichische Artificial Intelligence-Tagung, Igls, Tirol, 28. bis 30. Sept 1989, Proceedings, vol. 208 of Informatik-Fachberichte, Springer, pp 87\u201395","DOI":"10.1007\/978-3-642-74688-8_10"},{"key":"430_CR34","unstructured":"Flint A, Blaschko MB (2012) Perceptron learning of SAT. In: Bartlett PL, Pereira FNC, Burges CJC, L\u00e9on B, Weinberger KQ, (eds) Advances in neural information processing systems 25: 26th annual conference on neural information processing systems 2012. Proceedings of a meeting held Dec 3\u20136, 2012, Lake Tahoe, Nevada, United States, pp 2780\u20132788"},{"key":"430_CR35","doi-asserted-by":"publisher","first-page":"103572","DOI":"10.1016\/j.artint.2021.103572","volume":"301","author":"N Froleyks","year":"2021","unstructured":"Froleyks N, Heule M, Iser M, J\u00e4rvisalo M, Suda M (2021) SAT competition 2020. Artif Intell 301:103572","journal-title":"Artif Intell"},{"issue":"POPL","key":"430_CR36","doi-asserted-by":"publisher","first-page":"5:1","DOI":"10.1145\/3371073","volume":"4","author":"YMY Feldman","year":"2020","unstructured":"Feldman YMY, Immerman N, Sagiv M, Shoham S (2020) Complexity and information in invariant inference. Proc ACM Program Lang 4(POPL):5:1-5:29","journal-title":"Proc ACM Program Lang"},{"key":"430_CR37","doi-asserted-by":"crossref","unstructured":"First E, Rabe MN, Ringer T, Brun Y (2023) Baldur: whole-proof generation and repair with large language models. CoRR, abs\/2303.04910","DOI":"10.1145\/3611643.3616243"},{"key":"430_CR38","unstructured":"Fukunaga AS (2002) Automated discovery of composite SAT variable-selection heuristics. In: Dechter R, Kearns MJ, Sutton RS, (eds) proceedings of the eighteenth national conference on artificial intelligence and fourteenth conference on innovative applications of artificial intelligence, July 28 - August 1, 2002, Edmonton, Alberta, Canada, AAAI Press \/ The MIT Press, pp 641\u2013648"},{"key":"430_CR39","doi-asserted-by":"crossref","unstructured":"Fukunaga AS (2004) Evolving local search heuristics for SAT using genetic programming. In: Kalyanmoy D, Riccardo P, Wolfgang B, Hans-Georg B, Burke EK, Darwen PJ, Dasgupta D, Floreano D, Foster JA, Mark H, Owen H, Pier\u00a0Luca L, Lee S, Andrea T, Dirk T, Tyrrell AM, (eds) Genetic and evolutionary computation-GECCO 2004, genetic and evolutionary computation conference, Seattle, WA, USA, June 26\u201330, 2004, Proceedings, Part II, volume 3103 of Lecture Notes in Computer Science, Springer, pp 483\u2013494","DOI":"10.1007\/978-3-540-24855-2_59"},{"issue":"1","key":"430_CR40","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1162\/evco.2008.16.1.31","volume":"16","author":"AS Fukunaga","year":"2008","unstructured":"Fukunaga AS (2008) Automated discovery of local search heuristics for satisfiability testing. Evol Comput 16(1):31\u201361","journal-title":"Evol Comput"},{"key":"430_CR41","volume-title":"Adaptive computation and machine learning","author":"JG Ian","year":"2016","unstructured":"Ian JG, Yoshua B, Courville AC (2016) Deep Learning. Adaptive computation and machine learning. MIT Press, Cambridge"},{"key":"430_CR42","first-page":"303","volume":"50","author":"SA Goldman","year":"1992","unstructured":"Goldman SA, Kearns MJ (1992) On the complexity of teaching. J Comput Syst Sci 50:303\u2013314","journal-title":"J Comput Syst Sci"},{"key":"430_CR43","unstructured":"Gupta A (2006) Learning Abstractions for Model Checking. PhD thesis, Carnegie Mellon University, June"},{"key":"430_CR44","doi-asserted-by":"crossref","unstructured":"Hutter F, Babic D, Hoos HH, Hu AJ (2007) Boosting verification by automatic tuning of decision procedures. In: 7th international conference on formal methods in computer-aided design (FMCAD), IEEE Computer Society, pp 27\u201334","DOI":"10.1109\/FAMCAD.2007.9"},{"issue":"2","key":"430_CR45","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1109\/TSSC.1968.300136","volume":"4","author":"PE Hart","year":"1968","unstructured":"Hart PE, Nilsson NJ, Raphael B (1968) A formal basis for the heuristic determination of minimum cost paths. IEEE Trans Syst Sci Cybern 4(2):100\u2013107","journal-title":"IEEE Trans Syst Sci Cybern"},{"issue":"6","key":"430_CR46","doi-asserted-by":"publisher","first-page":"807","DOI":"10.1561\/2200000081","volume":"14","author":"SB Holden","year":"2021","unstructured":"Holden SB (2021) Machine learning for automated theorem proving: learning to solve SAT and QSAT. Found Trends Mach Learn 14(6):807\u2013989","journal-title":"Found Trends Mach Learn"},{"key":"430_CR47","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/BF00339943","volume":"52","author":"JJ Hopfield","year":"1985","unstructured":"Hopfield JJ, Tank DW (1985) Neural computation of decisions in optimization problems. Biol Cybern 52:141\u2013152","journal-title":"Biol Cybern"},{"key":"430_CR48","doi-asserted-by":"crossref","unstructured":"Jha S, Gulwani S, Seshia SA, Tiwari A (2010) Oracle-guided component-based program synthesis. In: Proceedings of the 32nd international conference on software engineering (ICSE), pp 215\u2013224","DOI":"10.1145\/1806799.1806833"},{"key":"430_CR49","doi-asserted-by":"crossref","unstructured":"Jha S, Gulwani S, Seshia SA, Tiwari A (2010) Synthesizing switching logic for safety and dwell-time requirements. In: proceedings of the international conference on cyber-physical systems (ICCPS), pp 22\u201331","DOI":"10.1145\/1795194.1795198"},{"key":"430_CR50","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1016\/0743-7315(89)90068-3","volume":"6","author":"JL Johnson","year":"1989","unstructured":"Johnson JL (1989) A neural network approach to the 3-satisfiability problem. J Parallel Distributed Comput 6:435\u2013449","journal-title":"J Parallel Distributed Comput"},{"issue":"7","key":"430_CR51","doi-asserted-by":"publisher","first-page":"693","DOI":"10.1007\/s00236-017-0294-5","volume":"54","author":"S Jha","year":"2017","unstructured":"Jha S, Seshia SA (2017) A theory of formal synthesis via inductive learning. Acta Inform 54(7):693\u2013726","journal-title":"Acta Inform"},{"issue":"9","key":"430_CR52","doi-asserted-by":"publisher","first-page":"4166","DOI":"10.1109\/TNNLS.2020.3017010","volume":"32","author":"S Kim","year":"2021","unstructured":"Kim S, Lu PY, Mukherjee S, Gilbert M, Jing L, \u010ceperi\u0107 V, Solja\u010di\u0107 M (2021) Integration of neural network-based symbolic regression in deep learning for scientific discovery. IEEE Trans Neural Netw Learn Syst 32(9):4166\u20134177","journal-title":"IEEE Trans Neural Netw Learn Syst"},{"key":"#cr-split#-430_CR53.1","unstructured":"Kautz HA, Selman B (1992) Planning as satisfiability. In: Bernd N,"},{"key":"#cr-split#-430_CR53.2","unstructured":"(ed) 10th European conference on artificial intelligence, ECAI 92, Vienna, Austria, August 3-7, 1992. Proceedings, John Wiley and Sons, pp 359-363"},{"key":"430_CR54","doi-asserted-by":"crossref","unstructured":"Kurshan R (1994) Automata-theoretic verification of coordinating processes. In: 11th international conference on analysis and optimization of systems\u2013discrete event systems, vol. 199 of LNCS, Springer, pp 16\u201328","DOI":"10.1007\/BFb0033528"},{"key":"430_CR55","unstructured":"Lewkowycz A, Andreassen A, Dohan D, Dyer E, Michalewski H, Ramasesh VV, Slone A, Anil C, Schlag I, Gutman-Solo T, Wu Y, Neyshabur B, Gur-Ari G, Misra V (2022) Solving quantitative reasoning problems with language models. CoRR, abs\/2206.14858"},{"key":"430_CR56","doi-asserted-by":"crossref","unstructured":"Liang JH, Ganesh V, Poupart P, Czarnecki K (2016) Learning rate based branching heuristic for SAT solvers. In: Nadia C, Daniel LB, (eds) Theory and applications of satisfiability testing\u2013SAT 2016, Cham. Springer International Publishing, pp 123\u2013140","DOI":"10.1007\/978-3-319-40970-2_9"},{"key":"430_CR57","unstructured":"Liang JH (2018) Machine learning for SAT solvers. PhD thesis, University of Waterloo, Canada"},{"key":"430_CR58","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1016\/S1571-0653(04)00332-4","volume":"9","author":"G Lagoudakis Michail","year":"2001","unstructured":"Lagoudakis Michail G, Littman Michael L (2001) Learning to select branching rules in the DPLL procedure for satisfiability. Electron Notes Discrete Math 9:344\u2013359","journal-title":"Electron Notes Discrete Math"},{"key":"430_CR59","doi-asserted-by":"crossref","unstructured":"Liang JH, Oh C, Mathew M, Thomas C, Li C, Ganesh V (2018) Machine learning-based restart policy for CDCL SAT solvers. In: theory and applications of satisfiability testing-SAT 2018 - 21st international conference, SAT 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9\u201312, 2018, Proceedings, pp 94\u2013110","DOI":"10.1007\/978-3-319-94144-8_6"},{"key":"430_CR60","unstructured":"Lederman G, Rabe MN, Seshia S, Lee EA (2020) Learning heuristics for quantified boolean formulas through reinforcement learning. In: 8th international conference on learning representations (ICLR), April"},{"key":"430_CR61","doi-asserted-by":"crossref","unstructured":"Lorenz JH, W\u00f6rz F (2020) On the effect of learned clauses on stochastic local search. In: Luca P, Martina S, (eds) Theory and applications of satisfiability testing-SAT 2020\u201323rd international conference, Alghero, Italy, July 3\u201310, 2020, Proceedings, vol. 12178 of lecture notes in computer science, Springer, pp 89\u2013106","DOI":"10.1007\/978-3-030-51825-7_7"},{"key":"430_CR62","volume-title":"Mitchell","author":"M Tom","year":"1997","unstructured":"Tom M (1997) Mitchell. McGraw-Hill, Machine Learning"},{"key":"430_CR63","doi-asserted-by":"crossref","unstructured":"Marques-Silva JP, Sakallah KA (1996) GRASP-A new search algorithm for satisfiability. In: proceedings of the 1996 IEEE\/ACM international conference on computer-aided design, ICCAD \u201996, Washington, DC, USA. IEEE Computer Society, pp 220\u2013227","DOI":"10.1109\/ICCAD.1996.569607"},{"issue":"1","key":"430_CR64","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z Manna","year":"1980","unstructured":"Manna Z, Waldinger R (1980) A deductive approach to program synthesis. ACM Trans Program Lang Syst (TOPLAS) 2(1):90\u2013121","journal-title":"ACM Trans Program Lang Syst (TOPLAS)"},{"key":"#cr-split#-430_CR65.1","doi-asserted-by":"crossref","unstructured":"Nejati S, Frioux LL, Ganesh V (2020) A machine learning based splitting heuristic for divide-and-conquer solvers. In: Helmut S,","DOI":"10.1007\/978-3-030-58475-7_52"},{"key":"#cr-split#-430_CR65.2","unstructured":"(ed) Principles and practice of constraint programming-26th international conference, CP 2020, Louvain-la-Neuve, Belgium, Sept 7-11, 2020, Proceedings, vol. 12333 of lecture notes in computer science, Springer, pp 899-916"},{"key":"430_CR66","unstructured":"OpenAI. GPT-4 technical report. CoRR, abs\/2303.08774, 2023"},{"key":"430_CR67","unstructured":"Panju M (2021) Automated Knowledge Discovery using Neural Networks. PhD thesis, University of Waterloo, Ontario, Canada"},{"key":"430_CR68","doi-asserted-by":"crossref","unstructured":"Polgreen E, Cheang K, Gaddamadugu P, Godbole A, Laeufer K, Lin S, Manerkar YA, Mora F, Seshia SA (2022) UCLID5: multi-modal formal modeling, verification, and synthesis. In: computer aided verification-34th international conference (CAV), vol. 13371 of lecture notes in computer science, Springer, pp 538\u2013551","DOI":"10.1007\/978-3-031-13185-1_27"},{"issue":"2","key":"430_CR69","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1016\/j.artint.2010.10.002","volume":"175","author":"K Pipatsrisawat","year":"2011","unstructured":"Pipatsrisawat K, Darwiche A (2011) On the power of clause-learning SAT solvers as resolution engines. Artif Intell 175(2):512\u2013525","journal-title":"Artif Intell"},{"issue":"1","key":"430_CR70","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/s10844-021-00666-5","volume":"58","author":"P Andrei","year":"2022","unstructured":"Andrei P, Polat ES, Alexander F, Mathias U, M\u00fcsl\u00fcm A, Viet-Man L, Klaus P, Martin E, Trang TTN (2022) An overview of machine learning techniques in constraint solving. J Intell Inf Syst 58(1):91\u2013118","journal-title":"J Intell Inf Syst"},{"key":"430_CR71","doi-asserted-by":"crossref","unstructured":"Pimpalkhare N, Mora F, Polgreen E, Seshia SA (2021) MedleySolver: online SMT algorithm selection. In: 24th international conference on theory and applications of satisfiability testing (SAT), vol. 12831 of lecture notes in computer science, Springer, pp 453\u2013470","DOI":"10.1007\/978-3-030-80223-3_31"},{"key":"430_CR72","unstructured":"Pogancic MV, Paulus A, Musil V, Martius G, Rol\u00ednek M (2020) Differentiation of blackbox combinatorial solvers. In: 8th international conference on learning representations, ICLR 2020, Addis Ababa, Ethiopia, April 26\u201330, 2020. OpenReview.net"},{"key":"430_CR73","doi-asserted-by":"crossref","unstructured":"Polgreen E, Reynolds A, Seshia SA (2022) Satisfiability and synthesis modulo oracles. In: Proceedings of the 23rd international conference on verification, model checking, and abstract interpretation (VMCAI)","DOI":"10.1007\/978-3-030-94583-1_13"},{"key":"430_CR74","volume-title":"Cognitive technologies","author":"L De Raedt","year":"2008","unstructured":"De Raedt L (2008) Logical and relational learning. Cognitive technologies. Springer, Berlin"},{"key":"430_CR75","volume-title":"Artificial intelligence: a modern approach","author":"S Russell","year":"2020","unstructured":"Russell S, Norvig P (2020) Artificial intelligence: a modern approach, 4th edn. Pearson, London","edition":"4"},{"key":"430_CR76","unstructured":"Rossi F, van Beek P, Walsh T (2006) editors. Handbook of Constraint Programming, vol.\u00a02 of Foundations of Artificial Intelligence. Elsevier"},{"key":"430_CR77","volume-title":"Adaptive computation and machine learning","author":"SS Richard","year":"1998","unstructured":"Richard SS, Andrew GB (1998) Reinforcement learning-an introduction. Adaptive computation and machine learning. MIT Press, Cambridge"},{"key":"430_CR78","unstructured":"Seshia SA (2005) Adaptive eager boolean encoding for arithmetic reasoning in verification. PhD thesis, Carnegie Mellon University"},{"key":"430_CR79","doi-asserted-by":"crossref","unstructured":"Seshia SA (2012) Sciduction: combining induction, deduction, and structure for verification and synthesis. In: proceedings of the design automation conference (DAC), pp 356\u2013365","DOI":"10.1145\/2228360.2228425"},{"issue":"11","key":"430_CR80","doi-asserted-by":"publisher","first-page":"2036","DOI":"10.1109\/JPROC.2015.2471838","volume":"103","author":"SA Seshia","year":"2015","unstructured":"Seshia SA (2015) Combining induction, deduction, and structure for verification and synthesis. Proc IEEE 103(11):2036\u20132051","journal-title":"Proc IEEE"},{"key":"430_CR81","unstructured":"Selsam D, Lamm M, B\u00fcnz B, Liang P, de\u00a0Moura L, Dill DL (2019) Learning a SAT solver from single-bit supervision. In: 7th international conference on learning representations, ICLR 2019, New Orleans, LA, USA, May 6\u20139, 2019. OpenReview.net"},{"key":"430_CR82","doi-asserted-by":"crossref","unstructured":"Solar-Lezama A, Tancau L, Bod\u00edk R, Seshia SA, Saraswat VA (2006) Combinatorial sketching for finite programs. In: proceedings of the 12th international conference on architectural support for programming languages and operating systems (ASPLOS), ACM Press, pp 404\u2013415","DOI":"10.1145\/1168857.1168907"},{"key":"430_CR83","doi-asserted-by":"crossref","unstructured":"Scott J, Niemetz A, Preiner M, Nejati S, Ganesh V (2021) Machsmt: a machine learning-based algorithm selector for SMT solvers. In: Jan\u00a0Friso G, Kim\u00a0Guldstrand L, (eds) Tools and algorithms for the construction and analysis of systems-27th international conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27\u2013April 1, 2021, Proceedings, Part II, vol. 12652 of Lecture Notes in Computer Science, Springer, pp 303\u2013325","DOI":"10.1007\/978-3-030-72013-1_16"},{"key":"430_CR84","doi-asserted-by":"crossref","unstructured":"Scott J, Panju M, Ganesh V (2020) LGML: logic guided machine learning. In: the thirty-fourth AAAI conference on artificial intelligence, AAAI 2020, the thirty-second innovative applications of artificial intelligence conference, IAAI 2020, the tenth AAAI symposium on educational advances in artificial intelligence, EAAI 2020, New York, NY, USA, Feb 7\u201312, 2020, AAAI Press, pp 13909\u201313910","DOI":"10.1609\/aaai.v34i10.7227"},{"key":"430_CR85","unstructured":"Marques SJP, Sakallah KA (1996) GRASP-a new search algorithm for satisfiability. In: Rutenbar RA, Otten RHJM, (eds) proceedings of the 1996 IEEE\/ACM international conference on computer-aided design, ICCAD 1996, San Jose, CA, USA, Nov 10\u201314, 1996, IEEE Computer Society \/ ACM, pp 220\u2013227"},{"key":"430_CR86","doi-asserted-by":"crossref","unstructured":"Seshia SA, Subramanyan P (2018) UCLID5: integrating modeling, verification, synthesis, and learning. In: proceedings of the 15th ACM\/IEEE international conference on formal methods and models for codesign (MEMOCODE)","DOI":"10.1109\/MEMCOD.2018.8556946"},{"issue":"7","key":"430_CR87","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1145\/3503914","volume":"65","author":"SA Seshia","year":"2022","unstructured":"Seshia SA, Sadigh D, Sastry SS (2022) Toward verified artificial intelligence. Commun ACM 65(7):46\u201355","journal-title":"Commun ACM"},{"key":"430_CR88","doi-asserted-by":"crossref","unstructured":"Seshia SA, Sharygina N, Tripakis S (2018) Modeling for verification. In: Clarke EM, Thomas H, Helmut V, (eds) Handbook of Model Checking, chapter\u00a03. Springer","DOI":"10.1007\/978-3-319-10575-8_3"},{"issue":"3","key":"430_CR89","doi-asserted-by":"publisher","first-page":"197","DOI":"10.3233\/AIC-210084","volume":"34","author":"Md Sarker","year":"2021","unstructured":"Sarker Md, Kamruzzaman ZL, Aaron E, Pascal H (2021) Neuro-symbolic artificial intelligence. AI Commun 34(3):197\u2013209","journal-title":"AI Commun"},{"key":"430_CR90","doi-asserted-by":"crossref","unstructured":"van Harmelen F, Lifschitz V, Porter BW (2008) (eds) Handbook of Knowledge Representation, vol. \u00a03 of Foundations of Artificial Intelligence. Elsevier","DOI":"10.1016\/S1574-6526(07)03001-5"},{"key":"430_CR91","unstructured":"The Verification of Neural Networks Library (VNN-LIB). www.vnnlib.org, 2019"},{"key":"430_CR92","unstructured":"Wang PW, Donti PL, Wilder B, Zico KJ (2019) Satnet: bridging deep learning and logical reasoning using a differentiable satisfiability solver. In: Kamalika C, Ruslan S, (eds) proceedings of the 36th international conference on machine learning, ICML 2019, 9\u201315 June 2019, Long Beach, California, USA, vol.\u00a097 of Proceedings of Machine Learning Research, PMLR, pp 6545\u20136554"},{"issue":"10","key":"430_CR93","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1145\/3448248","volume":"64","author":"MW Jeannette","year":"2021","unstructured":"Jeannette MW (2021) Trustworthy AI. Commun ACM 64(10):64\u201371","journal-title":"Commun ACM"},{"issue":"1","key":"430_CR94","first-page":"565","volume":"32","author":"X Lin","year":"2008","unstructured":"Lin X, Hutter F, Hoos HH, Leyton-Brown K (2008) SATzilla: portfolio-based algorithm selection for SAT. J Artif Intell Res 32(1):565\u2013606","journal-title":"J Artif Intell Res"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00430-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-023-00430-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00430-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,15]],"date-time":"2023-12-15T02:26:13Z","timestamp":1702607173000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-023-00430-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6]]},"references-count":96,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022,6]]}},"alternative-id":["430"],"URL":"https:\/\/doi.org\/10.1007\/s10703-023-00430-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,6]]},"assertion":[{"value":"17 October 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 May 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 June 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}