{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T17:19:08Z","timestamp":1774891148756,"version":"3.50.1"},"reference-count":253,"publisher":"Emerald","issue":"6","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,11,22]]},"abstract":"<jats:p>The decision problem for Boolean satisfiability, generally referred to as SAT, is the archetypal NP-complete problem, and encodings of many problems of practical interest exist allowing them to be treated as SAT problems. Its generalization to quantified SAT (QSAT) is PSPACE-complete, and is useful for the same reason. Despite the computational complexity of SAT and QSAT, methods have been developed allowing large instances to be solved within reasonable resource constraints. These techniques have largely exploited algorithmic developments; however machine learning also exerts a significant influence in the development of state-of- the-art solvers. Here, the application of machine learning is delicate, as in many cases, even if a relevant learning problem can be solved, it may be that incorporating the result into a SAT or QSAT solver is counterproductive, because the run-time of such solvers can be sensitive to small implementation changes. The application of better machine learning methods in this area is thus an ongoing challenge, with characteristics unique to the field. This work provides a comprehensive review of the research to date on incorporating machine learning into SAT and QSAT solvers, as a resource for those interested in further advancing the field.<\/jats:p>","DOI":"10.1561\/2200000081","type":"journal-article","created":{"date-parts":[[2021,11,22]],"date-time":"2021-11-22T03:06:36Z","timestamp":1637550396000},"page":"807-889","source":"Crossref","is-referenced-by-count":15,"title":["Machine Learning for Automated Theorem Proving: Learning to Solve SAT and QSAT"],"prefix":"10.1561","volume":"14","author":[{"given":"Sean B.","family":"Holden","sequence":"first","affiliation":[{"name":"University of Cambridge ,","place":["UK"]}]}],"member":"140","published-online":{"date-parts":[[2021,11,22]]},"reference":[{"key":"2026033012252319800_ref001","first-page":"185","volume-title":"An Evolutionary Local Search Algorithm for the Satisfiability Problem","author":"Aksoy","year":"2005"},{"key":"2026033012252319800_ref002","first-page":"41","volume-title":"Selecting the Right Heuristic Algorithm: Runtime Performance Predictors","author":"Allan","year":"1996"},{"key":"2026033012252319800_ref003","first-page":"232","volume-title":"A Multicore Tool for Constraint Solving","author":"Amadini","year":"2015"},{"key":"2026033012252319800_ref004","volume-title":"Learning To Solve Circuit-SAT: An Unsupervised Differentiable Approach","author":"Amizadeh","year":"2019"},{"key":"2026033012252319800_ref005","first-page":"107","volume-title":"The Fractal Dimension of SAT Formulas","author":"Ans\u00f3tegui","year":"2014"},{"key":"2026033012252319800_ref006","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/j.jal.2016.11.004","article-title":"Structure instances for SAT instances classification","volume":"23","author":"Ans\u00f3tegui","year":"2017","journal-title":"Journal of Applied Logic."},{"key":"2026033012252319800_ref007","first-page":"410","volume-title":"The Community Structure of SAT Formulas","author":"Ans\u00f3tegui","year":"2012"},{"key":"2026033012252319800_ref008","first-page":"142","volume-title":"A Gender-Based Genetic Algorithm for the Automatic Configuration of Algorithms","author":"Ans\u00f3tegui","year":"2009"},{"key":"2026033012252319800_ref009","volume-title":"Pattern Recognition and Machine Learning.","author":"Anthony","year":"2009"},{"issue":"1","key":"2026033012252319800_ref010","doi-asserted-by":"crossref","DOI":"10.1142\/S0218213018400018","article-title":"On the Glucose SAT Solver","volume":"27","author":"Audemard","year":"2018","journal-title":"International Journal on Artificial Intelligence Tools."},{"key":"2026033012252319800_ref011","first-page":"399","volume-title":"Predicting learnt clauses quality in modern SAT solvers","author":"Audemard","year":"2009"},{"key":"2026033012252319800_ref012","first-page":"332","volume-title":"Gambling in a rigged casino: The adversarial multi-armed bandit problem","author":"Auer","year":"1995"},{"key":"2026033012252319800_ref013","volume-title":"Layer Normalization","author":"Ba","year":"2016"},{"key":"2026033012252319800_ref014","first-page":"366","volume-title":"Structural Abstraction of Software Verification Conditions","author":"Babi\u0107","year":"2007"},{"key":"2026033012252319800_ref015","first-page":"37","volume-title":"Generating SAT Local Search Heuristics Using a GP Hyper-Heuristic Framework","author":"Bader-El-Den","year":"2007"},{"key":"2026033012252319800_ref016","first-page":"3342","volume-title":"Analysis and extension of the Inc* on the satisfiability testing problem","author":"Bader-El-Den","year":"2008"},{"key":"2026033012252319800_ref017","first-page":"1","volume-title":"Genetic Programming Theory and Practice VI.","author":"Bader-El-Den","year":"2008"},{"key":"2026033012252319800_ref018","first-page":"194","volume-title":"Inc*: An Incremental Approach for Improving Local Search Heuristics","author":"Bader-El-Den","year":"2008"},{"key":"2026033012252319800_ref019","first-page":"1068","volume-title":"A Comparison of Evolutionary Methods for the Discovery of Local Search Heuristics","author":"Bain","year":"2005"},{"key":"2026033012252319800_ref020","first-page":"732","volume-title":"Evolving VariableOrdering Heuristics for Constrained Optimisation","author":"Bain","year":"2005"},{"key":"2026033012252319800_ref021","first-page":"1359","volume-title":"Why Asynchronous Parallel Evolution is the Future of Hyper-heuristics: A CDCL SAT Solver Case Study","author":"Bertels","year":"2016"},{"key":"2026033012252319800_ref022","first-page":"7549","volume-title":"MA thesis.","author":"Bertels","year":"2016"},{"key":"2026033012252319800_ref023","first-page":"28","volume-title":"Adaptive Restart Strategies for Conflict Driven SAT Solvers","author":"Biere","year":"2008"},{"issue":"2-4","key":"2026033012252319800_ref024","doi-asserted-by":"crossref","first-page":"75","DOI":"10.3233\/SAT190039","article-title":"PicoSAT Essentials","volume":"4","author":"Biere","year":"2008","journal-title":"Journal of Satisfiability, Boolean Modeling and Computation."},{"key":"2026033012252319800_ref025","doi-asserted-by":"crossref","first-page":"197","DOI":"10.21236\/ADA360973","volume-title":"Symbolic Model Checking without BDDs","author":"Biere","year":"1999"},{"key":"2026033012252319800_ref026","volume-title":"CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling Entering the SAT Competition 2020","author":"Biere","year":"2020"},{"key":"2026033012252319800_ref027","first-page":"405","volume-title":"Evaluating CDCL Variable Scoring Schemes","author":"Biere","year":"2015"},{"key":"2026033012252319800_ref028","first-page":"1","volume-title":"Evaluating CDCL Restart Schemes","author":"Biere","year":"2019"},{"key":"2026033012252319800_ref029","volume-title":"Handbook of Satisfiability. Vol. 85. Frontiers in Artificial Intel ligence and Applications.","author":"Biere","year":"2009"},{"key":"2026033012252319800_ref030","volume-title":"Hyperparameter Optimization: Foundations, Algorithms, Best Practices and Open Challenges","author":"Bischl","year":"2021"},{"key":"2026033012252319800_ref031","volume-title":"Pattern Recognition and Machine Learning.","author":"Bishop","year":"2006"},{"issue":"1-5","key":"2026033012252319800_ref032","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/s10817-018-9455-7","article-title":"A Verified SAT Solver Framework with Learn, Forget, Restart and Incrementality","volume":"61","author":"Blanchette","year":"2018","journal-title":"Journal of Automated Reasoning."},{"key":"2026033012252319800_ref033","doi-asserted-by":"crossref","DOI":"10.1088\/1742-5468\/2008\/10\/P10008","article-title":"Fast unfolding of communities in large networks","volume-title":"Journal of Statistical Mechanics: Theory and Experiment.","author":"Blondel","year":"2008"},{"key":"2026033012252319800_ref034","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511804076","volume-title":"Computability and Logic.","author":"Boolos","year":"2007","edition":"5th"},{"key":"2026033012252319800_ref035","volume-title":"PhD thesis.","author":"Boyan","year":"1998"},{"key":"2026033012252319800_ref036","first-page":"3","volume-title":"Learning Evaluations Functions for Global Optimization and Boolean Satisfiability","author":"Boyan","year":"1998"},{"key":"2026033012252319800_ref037","first-page":"77","article-title":"Learning Evaluation Functions to Improve Optimization by Local Search","volume":"1","author":"Boyan","year":"2000","journal-title":"Journal of Machine Learning Research."},{"issue":"1","key":"2026033012252319800_ref038","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1023\/A:1010933404324","article-title":"Random Forests","volume":"45","author":"Breiman","year":"2001","journal-title":"Machine Learning."},{"key":"2026033012252319800_ref039","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/s10817-014-9301-5","article-title":"Machine Learning for First-Order Theorem Proving: Learning to Select a Good Heuristic","volume":"53","author":"Bridge","year":"2014","journal-title":"Journal of Automated Reasoning."},{"key":"2026033012252319800_ref040","volume-title":"Graph Neural Networks and Boolean Satisfiability","author":"B\u00fcnz","year":"2017"},{"key":"2026033012252319800_ref041","volume-title":"Predicting Propositional Satisfiabilty via End-to-End Learning","author":"Cameron","year":"2020"},{"key":"2026033012252319800_ref042","first-page":"15","volume-title":"OASC-2017: *Zilla Submission","author":"Cameron","year":"2017"},{"key":"2026033012252319800_ref043","volume-title":"Using Rewarding Mechanisms for Improving Branching Heuristics","author":"Carvalho","year":"2004"},{"key":"2026033012252319800_ref044","doi-asserted-by":"crossref","DOI":"10.1109\/ISKE.2017.8258780","volume-title":"Adding a LBD-based Rewarding Mechanism in Branching Heuristic for SAT Solvers","author":"Chang","year":"2017"},{"issue":"1","key":"2026033012252319800_ref045","doi-asserted-by":"crossref","first-page":"334","DOI":"10.2991\/ijcis.2019.125905649","article-title":"A New Rewarding Mechanism for Branching Heuristic in SAT Solvers","volume":"12","author":"Chang","year":"2018","journal-title":"International Journal of Computational Intel ligence Systems."},{"key":"2026033012252319800_ref046","first-page":"41","volume-title":"MiniSAT with Classificationbased Preprocessing","author":"Chen","year":"2014"},{"key":"2026033012252319800_ref047","volume-title":"Graph Neural Reasoning May Fail in Certifying Boolean Unsatisfiability","author":"Chen","year":"2019"},{"issue":"1-3","key":"2026033012252319800_ref048","doi-asserted-by":"crossref","first-page":"99","DOI":"10.3233\/SAT190064","article-title":"Cache Conscious Data Structures for Boolean Satisfiability Solvers","volume":"6","author":"Chu","year":"2010","journal-title":"Journal of Satisfiability, Boolean Modeling and Computation."},{"key":"2026033012252319800_ref049","volume-title":"Top-Down Neural Model For Formulae","author":"Chvalovsky","year":"2019"},{"key":"2026033012252319800_ref050","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","article-title":"Bounded Model Checking Using Satisfiability Solving","volume":"19","author":"Clarke","year":"2001","journal-title":"Formal Methods in System Design."},{"issue":"4","key":"2026033012252319800_ref051","doi-asserted-by":"crossref","first-page":"661","DOI":"10.1137\/070710111","article-title":"Power-Law Distributions in Empirical Data","volume":"51","author":"Clauset","year":"2009","journal-title":"SIAM Review."},{"key":"2026033012252319800_ref052","first-page":"224","volume-title":"The Blackwel l Guide to Philosophical Logic.","author":"Dalen","year":"2001"},{"key":"2026033012252319800_ref053","first-page":"169","volume-title":"Learning as Search Optimization: Approximate Large Margin Methods for Structured Prediction","author":"Daum\u00e9","year":"2005"},{"issue":"7","key":"2026033012252319800_ref054","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","article-title":"A machine program for theorem-proving","volume":"5","author":"Davies","year":"1962","journal-title":"Communications of the ACM."},{"key":"2026033012252319800_ref055","first-page":"408","volume-title":"Bounded Model Checking with QBF","author":"Dershowitz","year":"2005"},{"key":"2026033012252319800_ref056","volume-title":"Satisfiability as a Classification Problem","author":"Devlin","year":"2008"},{"key":"2026033012252319800_ref057","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0711-5","volume-title":"A Probabilistic Theory of Pattern Recognition. Vol. 31. Stochastic Model ling and Applied Probability.","author":"Devroye","year":"1996"},{"key":"2026033012252319800_ref058","volume-title":"Pattern Classification.","author":"Duda","year":"2000","edition":"2nd"},{"issue":"3","key":"2026033012252319800_ref059","doi-asserted-by":"crossref","first-page":"795","DOI":"10.2307\/2275431","article-title":"Contraction-Free Sequent Calculi for Intuitionistic Logic","volume":"57","author":"Dyckhoff","year":"1992","journal-title":"The Journal of Symbolic Logic."},{"key":"2026033012252319800_ref060","first-page":"61","volume-title":"Effective Preprocessing in SAT Through Variable and Clause Elimination","author":"E\u00e9n","year":"2005"},{"key":"2026033012252319800_ref061","first-page":"502","volume-title":"An Extensible SAT-solver","author":"E\u00e9n","year":"2003"},{"key":"2026033012252319800_ref062","first-page":"417","volume-title":"Solving Advanced Reasoning Tasks using Quantified Boolean Formulas","author":"Egly","year":"2000"},{"key":"2026033012252319800_ref063","first-page":"1","volume-title":"Handbook of Heuristics.","author":"Emmerich","year":"2018"},{"key":"2026033012252319800_ref064","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139164542","volume-title":"Statistical Mechanics of Learning.","author":"Engel","year":"2001"},{"key":"2026033012252319800_ref065","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/978-3-642-74688-8_10","volume-title":"5. Osterreichische Aertificial-Intel ligence-Tagung.","author":"Ertel","year":"1989"},{"key":"2026033012252319800_ref066","article-title":"Can Neural Networks Understand Logical Entailment?","author":"Evans","year":"2018"},{"key":"2026033012252319800_ref067","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/s10817-020-09576-7","article-title":"Machine Learning Guidance for Connection Tableaux","volume":"65","author":"F\u00e4rber","year":"2021","journal-title":"Journal of Automated Reasoning."},{"key":"2026033012252319800_ref068","first-page":"3133","article-title":"Do we Need Hundreds of Classifiers to Solve Real World Classification Problems?","volume":"15","author":"Fern\u00e1ndez-Delgado","year":"2014","journal-title":"Journal of Machine Learning Research."},{"key":"2026033012252319800_ref069","first-page":"294","volume-title":"fCube: An Efficient Prover for Intuitionistic Propositional Logic","author":"Ferrari","year":"2010"},{"key":"2026033012252319800_ref070","first-page":"115","volume-title":"Online Learning of Search Heuristics","author":"Fink","year":"2007"},{"key":"2026033012252319800_ref071","first-page":"158","volume-title":"A verified SAT solver with watched literals using imperative HOL","author":"Fleury","year":"2018"},{"key":"2026033012252319800_ref072","first-page":"2771","volume-title":"Perceptron Learning of SAT","author":"Flint","year":"2012"},{"key":"2026033012252319800_ref073","first-page":"702","volume-title":"Solving the Station Repacking Problem","author":"Fr\u00e9chette","year":"2016"},{"issue":"3,4","key":"2026033012252319800_ref074","first-page":"175","article-title":"Feature-based learning of searchguiding heuristics for theorem proving","volume":"11","author":"Fuchs","year":"1998","journal-title":"AI Communications."},{"key":"2026033012252319800_ref075","first-page":"641","volume-title":"Automated Discovery of Composite SAT Variable-Selection Heuristics","author":"Fukunaga","year":"2002"},{"key":"2026033012252319800_ref076","first-page":"483","volume-title":"Evolving Local Search Heuristics for SAT Using Genetic Programming","author":"Fukunaga","year":"2004"},{"issue":"1","key":"2026033012252319800_ref077","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1162\/evco.2008.16.1.31","article-title":"Automated Discovery of Local Search Heuristics for Satisfiability Testing","volume":"16","author":"Fukunaga","year":"2008","journal-title":"Evolutionary Computation."},{"key":"2026033012252319800_ref078","first-page":"1478","volume-title":"Massively Parallel Evolution of SAT Heuristics","author":"Fukunaga","year":"2009"},{"key":"2026033012252319800_ref079","first-page":"792","volume-title":"Learning Restart Strategies","author":"Gagliolo","year":"2007"},{"key":"2026033012252319800_ref080","volume-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness.","author":"Garey","year":"1979"},{"key":"2026033012252319800_ref081","first-page":"174","volume-title":"On Upper-Confidence Bound Policies for Switching Bandit Problems","author":"Garivier","year":"2011"},{"key":"2026033012252319800_ref082","first-page":"1263","volume-title":"Neural message passing for Quantum chemistry","author":"Gilmer","year":"2017"},{"key":"2026033012252319800_ref083","unstructured":"Giunchiglia, E., M.Narizzano, L.Pulina, and A.Tacchella. (2005). \u201cQuantified Boolean Formulas satisfiability library (QBFLIB)\u201d. url: www.qbflib.org."},{"key":"2026033012252319800_ref084","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1613\/jair.1959","article-title":"Clause\/Term Resolution and Learning in the Evaluation of Quantified Boolean Formulas","volume":"26","author":"Giunchiglia","year":"2006","journal-title":"Journal of Artificial Intel ligence Research."},{"key":"2026033012252319800_ref085","first-page":"142","volume-title":"BerkMin: A fast and robust SAT solver","author":"Goldberg","year":"2002"},{"key":"2026033012252319800_ref086","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/S0004-3702(00)00081-3","article-title":"Algorithm portfolios","volume":"126","author":"Gomes","year":"2001","journal-title":"Artificial Intel ligence."},{"key":"2026033012252319800_ref087","volume-title":"Deep Learning.","author":"Goodfellow","year":"2016"},{"issue":"1","key":"2026033012252319800_ref088","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1162\/106365602317301763","article-title":"Evolutionary Algorithms for the Satisfiability Problem","volume":"10","author":"Gottlieb","year":"2002","journal-title":"Evolutionary Computation."},{"key":"2026033012252319800_ref089","first-page":"127","volume-title":"Mathematical Approaches to Polymer Sequence Analysis and Related Problems.","author":"Gra\u00e7a","year":"2010"},{"key":"2026033012252319800_ref090","doi-asserted-by":"crossref","first-page":"441","DOI":"10.3233\/FI-2014-1024","article-title":"Can Machine Learning Learn a Decision Oracle for NP Problems? A Test on SAT","volume":"131","author":"Grozea","year":"2014","journal-title":"Fundamenta Informaticae."},{"key":"2026033012252319800_ref091","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-35488-8","volume-title":"Feature Extraction: Foundations and Applications. Studies in Fuzziness and Soft Computing.","author":"Guyon","year":"2006"},{"key":"2026033012252319800_ref092","first-page":"133","volume-title":"Online Estimation of SAT Solving Runtime","author":"Haim","year":"2008"},{"key":"2026033012252319800_ref093","first-page":"312","volume-title":"Restart Strategy Selection Using Machine Learning Techniques","author":"Haim","year":"2009"},{"issue":"4","key":"2026033012252319800_ref094","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1142\/S0218213010000303","article-title":"Learning for Dynamic Subsumption","volume":"19","author":"Hamadi","year":"2010","journal-title":"International Journal on Artificial Intelligence Tools: Architectures, Languages, Algorithms."},{"issue":"3","key":"2026033012252319800_ref095","first-page":"1159","article-title":"Graph Representation Learning","volume":"14","author":"Hamilton","year":"2020","journal-title":"Synthesis Lectures on Artificial Intel ligence and Machine Learning."},{"key":"2026033012252319800_ref096","first-page":"209","volume-title":"On-The-Fly Clause Improvement","author":"Han","year":"2009"},{"key":"2026033012252319800_ref097","volume-title":"Enhancing SAT solvers with glue variable predictions","author":"Han","year":"2020"},{"key":"2026033012252319800_ref098","volume-title":"Learning cubing heuristics for SAT from DRAT proofs","author":"Han","year":"2020"},{"key":"2026033012252319800_ref099","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511576430","volume-title":"Handbook of Practical Logic and Automated Reasoning.","author":"Harrison","year":"2009"},{"key":"2026033012252319800_ref100","first-page":"1909","volume-title":"Deep Models of Interactions Across Sets","author":"Hartford","year":"2018"},{"key":"2026033012252319800_ref101","doi-asserted-by":"crossref","DOI":"10.1007\/978-0-387-84858-7","volume-title":"The Elements of Statistical Learning: Data Mining, Inference, and Prediction.","author":"Hastie","year":"2009","edition":"2nd"},{"key":"2026033012252319800_ref102","unstructured":"Heule, M., M.J\u00e4rvisalo, and M.Suda. (2019). The international SAT Competitions web page. url: http:\/\/www.satcompetition.org\/."},{"key":"2026033012252319800_ref103","first-page":"228","volume-title":"Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-And-Conquer","author":"Heule","year":"2016"},{"key":"2026033012252319800_ref104","first-page":"50","volume-title":"Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads","author":"Heule","year":"2011"},{"key":"2026033012252319800_ref105","first-page":"4864","volume-title":"Solving Very Hard Problems: Cube-and-Conquer, a Hybrid SAT Solving Method","author":"Heule","year":"2017"},{"issue":"8","key":"2026033012252319800_ref106","doi-asserted-by":"crossref","first-page":"1735","DOI":"10.1162\/neco.1997.9.8.1735","article-title":"Long Short-Term Memory","volume":"9","author":"Hochreiter","year":"1997","journal-title":"Neural Computation."},{"key":"2026033012252319800_ref107","first-page":"201","volume-title":"A short overview of modern parallel SAT-solvers","author":"Holldobler","year":"2011"},{"key":"2026033012252319800_ref108","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1023\/A:1022631118932","article-title":"Very Simple Classification Rules Perform Well on Most Commonly Used Datasets","volume":"11","author":"Holte","year":"1993","journal-title":"Machine Learning."},{"key":"2026033012252319800_ref109","first-page":"195","volume-title":"Portfolio-Based Algorithm Selection for Circuit QBFs","author":"Hoos","year":"2018"},{"key":"2026033012252319800_ref110","first-page":"661","volume-title":"On the Run-Time Behavious of Stochastic Local Search Algorithms for SAT","author":"Hoos","year":"1999"},{"key":"2026033012252319800_ref111","first-page":"283","volume-title":"SAT2000: Highlights of Satisfiability Research in the Year 2000.","author":"Hoos","year":"2000"},{"key":"2026033012252319800_ref112","unstructured":"Hoos, H. H. and T.St\u00fctzle. (2019). SATLIB\u2014The Satisfiability Library. url: https:\/\/www.cs.ubc.ca\/~hoos\/SATLIB\/."},{"key":"2026033012252319800_ref113","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/BF00339943","article-title":"\u2018Neural\u2019 Computation of Decisions in Optimization Problems","volume":"52","author":"Hopfield","year":"1985","journal-title":"Biological Cybernetics."},{"key":"2026033012252319800_ref114","doi-asserted-by":"crossref","first-page":"1235","DOI":"10.1162\/neco_a_01199","article-title":"A Review of Recurrent Neural Networks: LSTM Cells and Network Architectures","volume":"31","author":"Hu","year":"2019","journal-title":"Neural Computation."},{"key":"2026033012252319800_ref115","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1126\/science.275.5296.51","article-title":"An Economics Approach to Hard Computational Problems","volume":"275","author":"Huberman","year":"1997","journal-title":"Science."},{"key":"2026033012252319800_ref116","first-page":"27","volume-title":"Boosting Verification by Automatic Tuning of Decision Procedures","author":"Hutter","year":"2007"},{"key":"2026033012252319800_ref117","first-page":"213","volume-title":"Performance Prediction and Automated Tuning of Randomized and Parametric Algorithms","author":"Hutter","year":"2006"},{"key":"2026033012252319800_ref118","first-page":"507","volume-title":"Sequential Model-Based Optimization for General Algorithm Configuration","author":"Hutter","year":"2011"},{"key":"2026033012252319800_ref119","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1613\/jair.2861","article-title":"ParamILS: An Automatic Algorithm Configuration Framework","volume":"36","author":"Hutter","year":"2009","journal-title":"Journal of Artificial Intelligence Research."},{"key":"2026033012252319800_ref120","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-030-05318-5","volume-title":"Automated Machine Learning: Methods, Systems, Chal lenges. The Springer Series on Challenges in Machine Learning.","author":"Hutter","year":"2019"},{"key":"2026033012252319800_ref121","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.artint.2016.09.006","article-title":"The Configurable SAT Solver Challenge (CSSC)","volume":"243","author":"Hutter","year":"2017","journal-title":"Artificial Intel ligence."},{"key":"2026033012252319800_ref122","first-page":"233","volume-title":"Scaling and Probabilistic Smoothing: Efficient Dynamic Local Search for SAT","author":"Hutter","year":"2002"},{"key":"2026033012252319800_ref123","first-page":"617","volume-title":"Improving performance of CDCL SAT solvers by automated design of variable selection heuristics","author":"Illetskova","year":"2017"},{"key":"2026033012252319800_ref124","first-page":"6607","volume-title":"Towards Generalization in QBF Solving via Machine Learning","author":"Janota","year":"2018"},{"key":"2026033012252319800_ref125","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.artint.2016.01.004","article-title":"Solving QBF with counterexample guided refinement","volume":"234","author":"Janota","year":"2016","journal-title":"Artificial Intel li-gence."},{"key":"2026033012252319800_ref126","first-page":"355","volume-title":"Inprocessing Rules","author":"J\u00e4rvisalo","year":"2012"},{"key":"2026033012252319800_ref127","volume-title":"Neural heuristics for SAT solving","author":"Jaszczur","year":"2019"},{"issue":"1-4","key":"2026033012252319800_ref128","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BF01531077","article-title":"Solving propositional satisfiability problems","volume":"1","author":"Jeroslow","year":"1990","journal-title":"Annals of Mathematics and Artificial Intelligence."},{"key":"2026033012252319800_ref129","doi-asserted-by":"crossref","first-page":"435","DOI":"10.1016\/0743-7315(89)90068-3","article-title":"A Neural Network Approach to the 3-Satisfiability Problem","volume":"6","author":"Johnson","year":"1989","journal-title":"Journal of Parallel and Distributed Computing."},{"key":"2026033012252319800_ref130","first-page":"192","volume-title":"Experiments with Reduction Finding","author":"Jordan","year":"2013"},{"key":"2026033012252319800_ref131","first-page":"454","volume-title":"Algorithm Selection and Scheduling","author":"Kadioglu","year":"2011"},{"key":"2026033012252319800_ref132","first-page":"751","volume-title":"ISAC\u2014 Instance-Specific Algorithm Configuration","author":"Kadioglu","year":"2010"},{"issue":"282","key":"2026033012252319800_ref133","doi-asserted-by":"crossref","first-page":"457","DOI":"10.1080\/01621459.1958.10501452","article-title":"Nonparametric Estimation from Incomplete Observations","volume":"53","author":"Kaplan","year":"1958","journal-title":"Journal of the American Statistical Association."},{"key":"2026033012252319800_ref134","doi-asserted-by":"crossref","DOI":"10.1002\/9780470316801","volume-title":"Finding Groups in Data: An Introduction to Cluster Analysis. Wiley Series in Probability and Statistics.","author":"Kaufman","year":"1990"},{"key":"2026033012252319800_ref135","first-page":"359","volume-title":"Planning as Satisfiability","author":"Kautz","year":"1992"},{"key":"2026033012252319800_ref136","first-page":"1524","volume-title":"Deconstructing Planning as Satisfiability","author":"Kautz","year":"2006"},{"key":"2026033012252319800_ref137","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1016\/j.artint.2015.11.002","article-title":"SATenstein: Automatically building local search SAT solvers from components","volume":"232","author":"Khudabukhsh","year":"2016","journal-title":"Artificial Intel ligence."},{"key":"2026033012252319800_ref138","first-page":"765","volume-title":"Evolving a Neural Network-Based Decision and Search Heuristic for DPLL SAT Solvers","author":"Kibria","year":"2007"},{"key":"2026033012252319800_ref139","first-page":"331","volume-title":"Optimizing the Initialization of Dynamic Decision Heuristics in DPLL SAT Solvers Using Genetic Programming","author":"Kibria","year":"2006"},{"key":"2026033012252319800_ref140","volume-title":"Soft Computing Approaches to DPLL SAT Solver Optimization","author":"Kibria","year":"2011"},{"key":"2026033012252319800_ref141","volume-title":"Adam: A Method For Stochastic Optimization","author":"Kingma","year":"2015"},{"key":"2026033012252319800_ref142","first-page":"128","volume-title":"A Non-prenex, Non-clausal QBF Solver with Game-State Learning","author":"Klieber","year":"2010"},{"key":"2026033012252319800_ref143","first-page":"1137","volume-title":"A study of cross-validation and bootstrap for accuracy estimation and model selection","author":"Kohavi","year":"1995"},{"key":"2026033012252319800_ref144","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/978-3-319-50137-6_7","volume-title":"Data Mining and Constraint Programming: Foundations of a Cross-Disciplinary Approach.","author":"Kotthoff","year":"2016"},{"key":"2026033012252319800_ref145","volume-title":"Genetic Programming: On the Programming of Computers by Means of Natural Selection.","author":"Koza","year":"1992"},{"key":"2026033012252319800_ref146","volume-title":"Improving SAT Solver Heuristics with Graph Networks and Reinforcement Learning","author":"Kurin","year":"2019"},{"key":"2026033012252319800_ref147","volume-title":"Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning","author":"Kusumoto","year":"2018"},{"key":"2026033012252319800_ref148","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-015-7744-1","volume-title":"Simulated Annealing: Theory and Applications.","author":"van Laarhoven","year":"1987"},{"key":"2026033012252319800_ref149","first-page":"511","volume-title":"Algorithm Selection using Reinforcement Learning","author":"Lagoudakis","year":"2000"},{"key":"2026033012252319800_ref150","doi-asserted-by":"crossref","first-page":"344","DOI":"10.1016\/S1571-0653(04)00332-4","article-title":"Learning to Select Branching Rules in the DPLL Procedure for Satisfiability","volume":"9","author":"Lagoudakis","year":"2001","journal-title":"Electronic Notes in Discrete Mathematics."},{"key":"2026033012252319800_ref151","volume-title":"Learning Heuristics for Quantified Formulas through Deep Reinforcement Learning","author":"Lederman","year":"2019"},{"issue":"2","key":"2026033012252319800_ref152","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/BF00244282","article-title":"SETHEO: A high-performance theorem prover","volume":"8","author":"Letz","year":"1992","journal-title":"Journal of Automated Reasoning."},{"key":"2026033012252319800_ref153","first-page":"279","article-title":"Clause vivification by unit propagation in CDCL SAT Solvers","volume-title":"Artificial Intel ligence.","author":"Li","year":"2020"},{"key":"2026033012252319800_ref154","first-page":"3434","volume-title":"Exponential recency weighted average branching heuristic for SAT solvers","author":"Liang","year":"2016"},{"key":"2026033012252319800_ref155","first-page":"123","volume-title":"Learning Rate Based Branching Heuristic for SAT Solvers","author":"Liang","year":"2016"},{"key":"2026033012252319800_ref156","first-page":"94","volume-title":"Machine Learning-Based Restart Policy for CDCL SAT Solvers","author":"Liang","year":"2018"},{"key":"2026033012252319800_ref157","first-page":"119","volume-title":"An Empirical Study of Branching Heuristics Through the Lens of Global Learning Rate","author":"Liang","year":"2017"},{"issue":"1","key":"2026033012252319800_ref158","doi-asserted-by":"crossref","first-page":"745","DOI":"10.1613\/jair.4726","article-title":"Autofolio: an automatically configured algorithm selector","volume":"53","author":"Lindauer","year":"2015","journal-title":"Journal of Artificial Intel ligence Research."},{"key":"2026033012252319800_ref159","first-page":"276","volume-title":"Evaluating QBF Solvers: Quantifier Alternations Matter","author":"Lonsing","year":"2018"},{"key":"2026033012252319800_ref160","first-page":"1280","volume-title":"Deep Learning for Algorithm Portfolios","author":"Loreggia","year":"2016"},{"key":"2026033012252319800_ref161","first-page":"128","volume-title":"Optimal speedup of Las Vegas algorithms","author":"Luby","year":"1993"},{"key":"2026033012252319800_ref162","volume-title":"Linear and Nonlinear Programming.","author":"Luenberger","year":"2003"},{"key":"2026033012252319800_ref163","first-page":"703","volume-title":"An Effective Learnt Clause Minimization Approach for CDCL SAT Solvers","author":"Luo","year":"2017"},{"issue":"1-4","key":"2026033012252319800_ref164","first-page":"137","article-title":"Efficient data structures for backtrack search SAT solvers","volume":"43","author":"Lynce","year":"2005","journal-title":"Annals of Mathematics and Artificial Intel ligence."},{"key":"2026033012252319800_ref165","first-page":"104","volume-title":"Efficient Haplotype Inference with Boolean Satisfiability","author":"Lynce","year":"2006"},{"key":"2026033012252319800_ref166","first-page":"369","volume-title":"Non-Model-Based Algorithm Portfolios for SAT","author":"Malitsky","year":"2011"},{"key":"2026033012252319800_ref167","first-page":"512","volume-title":"Parallel SAT Solver Selection and Scheduling","author":"Malitsky","year":"2012"},{"key":"2026033012252319800_ref168","first-page":"608","volume-title":"Algorithm Portfolios Based on Cost-Sensitive Hierarchical Clustering","author":"Malitsky","year":"2013"},{"key":"2026033012252319800_ref169","volume-title":"Bayesian Optimization of Solver Parameters in CBMC","author":"Mangla","year":"2020"},{"key":"2026033012252319800_ref170","volume-title":"Formalization, Implementation and Verification of SAT Solvers","author":"Mari\u0107","year":"2009"},{"key":"2026033012252319800_ref171","first-page":"62","volume-title":"The Impact of Branching Heuristics in Propositional Satisfiability Algorithms","author":"Marques-Silva","year":"1999"},{"key":"2026033012252319800_ref172","first-page":"74","volume-title":"Practical Applications of Boolean Satisfiability","author":"Marques-Silva","year":"2008"},{"issue":"5","key":"2026033012252319800_ref173","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","article-title":"GRASP: a search algorithm for propositional satisfiability","volume":"48","author":"Marques-Silva","year":"1999","journal-title":"IEEE Transactions on Computers."},{"issue":"4","key":"2026033012252319800_ref174","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1145\/367177.367199","article-title":"Recursive functions of symbolic expressions and their computation by machine, Part I","volume":"3","author":"McCarthy","year":"1960","journal-title":"Communications of the ACM."},{"key":"2026033012252319800_ref175","volume-title":"Tech. rep.","author":"McCune","year":"2003"},{"key":"2026033012252319800_ref176","first-page":"174","volume-title":"Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic","author":"McLaughlin","year":"2008"},{"key":"2026033012252319800_ref177","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/BF00143877","article-title":"Automatically Configuring Constraint Satisfaction Programs: A Case Study","volume":"1","author":"Minton","year":"1996","journal-title":"Constraints: An International Journal."},{"key":"2026033012252319800_ref178","volume-title":"An Introduction to Genetic Algorithms.","author":"Mitchell","year":"1998"},{"key":"2026033012252319800_ref179","volume-title":"Machine Learning.","author":"Mitchell","year":"1997"},{"key":"2026033012252319800_ref180","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1038\/nature14236","article-title":"Human-level control through deep reinforcement learning","volume":"518","author":"Mnih","year":"2015","journal-title":"Nature."},{"key":"2026033012252319800_ref181","first-page":"530","volume-title":"Chaff: engineering an efficient SAT solver","author":"Moskewicz","year":"2001"},{"key":"2026033012252319800_ref182","volume-title":"Machine Learning: A Probabilistic Perspective.","author":"Murphy","year":"2012"},{"key":"2026033012252319800_ref183","first-page":"111","volume-title":"Chronological Backtracking","author":"Nadel","year":"2018"},{"key":"2026033012252319800_ref184","first-page":"494","volume-title":"The QBFEVAL Web Portal","author":"Narizzano","year":"2006"},{"key":"2026033012252319800_ref185","first-page":"120","volume-title":"Adaptive Restart and CEGAR-Based Solver for Inverting Cryptographic Hash Functions","author":"Nejati","year":"2017"},{"issue":"6","key":"2026033012252319800_ref186","doi-asserted-by":"crossref","first-page":"937977","DOI":"10.1145\/1217856.1217859","article-title":"Solving SAT and SAT Modulo Theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T)","volume":"53","author":"Nieuwenhuis","year":"2006","journal-title":"Journal of the ACM."},{"key":"2026033012252319800_ref187","first-page":"326","volume-title":"Instance-Based Selection of Policies for SAT Solvers","author":"Nikoli\u0107","year":"2009"},{"key":"2026033012252319800_ref188","doi-asserted-by":"crossref","first-page":"457","DOI":"10.1007\/s10462-011-9290-2","article-title":"Simple algorithm portfolio for SAT","volume":"40","author":"Nikoli\u0107","year":"2013","journal-title":"Artificial Intel ligence Review."},{"key":"2026033012252319800_ref189","first-page":"438","volume-title":"Understanding Random SAT: Beyond the Clauses-to-Variables Ratio","author":"Nudelman","year":"2004"},{"key":"2026033012252319800_ref190","volume-title":"Using Case-based Reasoning in an Algorithm Portfolio for Constraint Solving","author":"O\u2019Mahony","year":"2008"},{"key":"2026033012252319800_ref191","first-page":"307","volume-title":"Between SAT and UNSAT: The Fundamental Difference in CDCL SAT","author":"Oh","year":"2015"},{"key":"2026033012252319800_ref192","volume-title":"Heuristics: Intel ligent Search Strategies for Coimputer Problem Solving.","author":"Pearl","year":"1984"},{"key":"2026033012252319800_ref193","first-page":"298","volume-title":"Dependency Learning for QBF","author":"Peitl","year":"2017"},{"key":"2026033012252319800_ref194","first-page":"137","volume-title":"Using Genetic Improevement and Code Transplants to Specialise a C++ Program to a Problem Class","author":"Petke","year":"2014"},{"key":"2026033012252319800_ref195","first-page":"257","volume-title":"Applying Genetic Improvement to MiniSAT","author":"Petke","year":"2013"},{"key":"2026033012252319800_ref196","first-page":"743","volume-title":"MetaLearning by Landmarking Various Learning Algorithms","author":"Pfahringer","year":"2000"},{"key":"2026033012252319800_ref197","volume-title":"Types and Programming Languages.","author":"Pierce","year":"2002"},{"key":"2026033012252319800_ref198","first-page":"294","volume-title":"A Lightweight Component Caching Scheme for Satisfiability Solvers","author":"Pipatsrisawat","year":"2007"},{"key":"2026033012252319800_ref199","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1007\/978-1-4419-1665-5_13","volume-title":"Handbook of Metaheuristics.","author":"Pisinger","year":"2010"},{"key":"2026033012252319800_ref200","first-page":"574","volume-title":"A Multi-engine Solver for Quantified Boolean Formulas","author":"Pulina","year":"2007"},{"key":"2026033012252319800_ref201","doi-asserted-by":"crossref","first-page":"80","DOI":"10.1007\/s10601-008-9051-2","article-title":"A self-adaptive multi-engine solver for quantified Boolean formulas","volume":"14","author":"Pulina","year":"2009","journal-title":"Constraints."},{"key":"2026033012252319800_ref202","volume-title":"C4.5: Programs for Machine Learning.","author":"Quinlan","year":"1993","edition":"1st"},{"key":"2026033012252319800_ref203","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1023\/A:1022643204877","article-title":"Induction of Decision Trees","volume":"1","author":"Quinlan","year":"1986","journal-title":"Machine Learning."},{"key":"2026033012252319800_ref204","first-page":"375","volume-title":"Incremental Determinization","author":"Rabe","year":"2016"},{"key":"2026033012252319800_ref205","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/s10817-006-9060-z","article-title":"The ILTP Problem Library for Intuitionistic Logic","volume":"38","author":"Raths","year":"2007","journal-title":"Journal of Automated Reasoning."},{"key":"2026033012252319800_ref206","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1613\/jair.591","article-title":"Constructing Conditional Plans by a Theorem-Prover","volume":"10","author":"Rintanen","year":"1999","journal-title":"Journal of Artificial Intelligence Research."},{"issue":"3","key":"2026033012252319800_ref207","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1023\/A:1022607331053","article-title":"Learning Decision Lists","volume":"2","author":"Rivest","year":"1987","journal-title":"Machine Learning."},{"key":"2026033012252319800_ref208","volume-title":"Artificial Intelligence: A Modern Approach.","author":"Russell","year":"2020","edition":"4th"},{"key":"2026033012252319800_ref209","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511975509","volume-title":"Phase Transitions in Machine Learning.","author":"Saitta","year":"2011"},{"key":"2026033012252319800_ref210","first-page":"255","volume-title":"Learning to Solve QBF","author":"Samulowitz","year":"2007"},{"key":"2026033012252319800_ref211","volume-title":"Machine learning of strategies for efficiently solving QBF with abstraction refinement","author":"Santos Silva","year":"2019"},{"issue":"4","key":"2026033012252319800_ref212","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1080\/00401706.1979.10489811","article-title":"A Simple Method for Regression Analysis with Censored Data","volume":"21","author":"Schmee","year":"1979","journal-title":"Technometrics."},{"key":"2026033012252319800_ref213","volume-title":"Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic","author":"Sekiyama","year":"2017"},{"key":"2026033012252319800_ref214","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-030-02768-1_17","volume-title":"Automated proof synthesis for propositional logic with deep neural networks","author":"Sekiyama","year":"2018"},{"key":"2026033012252319800_ref215","first-page":"309","volume-title":"Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks","author":"Sekiyama","year":"2018"},{"key":"2026033012252319800_ref216","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1090\/dimacs\/026\/25","volume-title":"Cliques, Coloring and Satisfiability.","author":"Selman","year":"1996"},{"key":"2026033012252319800_ref217","first-page":"440","volume-title":"A New Method for Solving Hard Satisfiability Problems","author":"Selman","year":"1992"},{"key":"2026033012252319800_ref218","first-page":"336","volume-title":"Guiding High-Performance SAT Solvers with Unsat-Core Predictions","author":"Selsam","year":"2019"},{"key":"2026033012252319800_ref219","volume-title":"Learning a SAT Solver from Single-Bit Supervision","author":"Selsam","year":"2019"},{"key":"2026033012252319800_ref220","first-page":"417","volume-title":"Using Constraint Programming and Local Search Methods to Solve Vehicle Routing Problems","author":"Shaw","year":"1998"},{"key":"2026033012252319800_ref221","volume-title":"Support Vector Machines and Other Kernel-Based Learning Methods.","author":"Shawe-Taylor","year":"2000"},{"key":"2026033012252319800_ref222","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511809682","volume-title":"Kernel Methods for Pattern Analysis.","author":"Shawe-Taylor","year":"2004"},{"key":"2026033012252319800_ref223","volume-title":"A Probabilistic Architecture for Algorithm Portfolios","author":"Silverthorn","year":"2012"},{"key":"2026033012252319800_ref224","first-page":"167","volume-title":"Latent Class Models for Algorithm Portfolio Methods","author":"Silverthorn","year":"2010"},{"key":"2026033012252319800_ref225","volume-title":"Tech. rep.","author":"Singh","year":"2009"},{"key":"2026033012252319800_ref226","first-page":"371","volume-title":"CrystalBall: Gazing in the Black Box of SAT Solving","author":"Soos","year":"2019"},{"key":"2026033012252319800_ref227","first-page":"237","volume-title":"Minimizing Learned Clauses","author":"S\u00f6rensson","year":"2009"},{"key":"2026033012252319800_ref228","first-page":"1121","volume-title":"A NN Algorithm for Boolean Satisfiability Problems","author":"Spears","year":"1996"},{"key":"2026033012252319800_ref229","first-page":"1577","volume-title":"An online algorithm for maximizing submodular functions","author":"Streeter","year":"2008"},{"key":"2026033012252319800_ref230","first-page":"3104","article-title":"Sequence to Sequence Learning with Neural Networks","volume-title":"Advances in Neural Information Processing Systems (NIPS).","author":"Sutskever","year":"2014"},{"key":"2026033012252319800_ref231","volume-title":"Reinforcement Learning: An Introduction.","author":"Sutton","year":"2018","edition":"2nd"},{"issue":"1","key":"2026033012252319800_ref232","doi-asserted-by":"crossref","first-page":"155","DOI":"10.3233\/SAT190121","article-title":"CAQE and QuAbS: Abstraction based QBF solvers","volume":"11","author":"Tentrup","year":"2019","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation."},{"issue":"3","key":"2026033012252319800_ref233","doi-asserted-by":"crossref","first-page":"659","DOI":"10.1109\/TKDE.2002.1000348","article-title":"An instance-weighting method to induce costsensitive trees","volume":"14","author":"Ting","year":"2002","journal-title":"IEEE Transactions on Knowledge and Data Engineering."},{"key":"2026033012252319800_ref234","volume-title":"Learning Clause Deletion Heuristics with Reinforcement Learning","author":"Vaezipoor","year":"2020"},{"key":"2026033012252319800_ref235","doi-asserted-by":"crossref","DOI":"10.1007\/0-387-34239-7","volume-title":"Estimation of Dependencies based on Empirical Data.","author":"Vapnik","year":"2006"},{"key":"2026033012252319800_ref236","first-page":"1201","article-title":"Graph Kernels","volume":"11","author":"Vishwanathan","year":"2010","journal-title":"Journal of Machine Learning Research."},{"issue":"1-5","key":"2026033012252319800_ref237","article-title":"Are Random Forests Truly the Best Classifiers?","volume":"17","author":"Wainberg","year":"2016","journal-title":"Journal of Machine Learning Research."},{"key":"2026033012252319800_ref238","doi-asserted-by":"crossref","first-page":"4771","DOI":"10.1007\/s10462-021-10011-5","article-title":"How to tune the RBF SVM hyperparameters? An empirical evaluation of 18 search algorithms","volume":"54","author":"Wainer","year":"2021","journal-title":"Artificial Intel ligence Review."},{"key":"2026033012252319800_ref239","first-page":"6545","volume-title":"SATNet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver","author":"Wang","year":"2019"},{"key":"2026033012252319800_ref240","first-page":"422","volume-title":"DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs","author":"Wetzler","year":"2014"},{"issue":"3-4","key":"2026033012252319800_ref241","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1023\/A:1022672621406","article-title":"Simple statistical gradient-following algorithms for connectionist reinforcement learning","volume":"8","author":"Williams","year":"1992","journal-title":"Machine Learning."},{"key":"2026033012252319800_ref242","first-page":"615","volume-title":"The Unit Preference Strategy in Theorem Proving","author":"Wos","year":"1964"},{"key":"2026033012252319800_ref243","volume-title":"A Comprehensive Survey on Graph Neural Networks","author":"Wu","year":"2019"},{"key":"2026033012252319800_ref244","first-page":"696","volume-title":"Hierarchical Hardness Models for SAT","author":"Xu","year":"2007"},{"key":"2026033012252319800_ref245","first-page":"228","volume-title":"Evaluating Component Solver Contributions to Portfolio-Based Algorithm Selectors","author":"Xu","year":"2012"},{"key":"2026033012252319800_ref246","doi-asserted-by":"crossref","first-page":"565","DOI":"10.1613\/jair.2490","article-title":"SATzilla: Portfolio-based Algorithm Selection for SAT","volume":"32","author":"Xu","year":"2008","journal-title":"Journal of Artificial Intel ligence Research."},{"key":"2026033012252319800_ref247","first-page":"53","article-title":"SATzilla2009: an Automatic Algorithm Portfolio for SAT","volume-title":"SAT 2009 competa-tive events booklet.","author":"Xu","year":"2009"},{"key":"2026033012252319800_ref248","volume-title":"Tech. rep.","author":"Xu","year":"2012"},{"key":"2026033012252319800_ref249","first-page":"57","volume-title":"SATzilla2012: Improved Algorithm Selection Based on Cost-sensitive Classification Models","author":"Xu","year":"2012"},{"key":"2026033012252319800_ref250","volume-title":"Graph Neural Reasoning for 2-Quantified Boolean Formula Solvers","author":"Yang","year":"2019"},{"key":"2026033012252319800_ref251","first-page":"7992","volume-title":"Learning Local Search Heuristics for Boolean Satisfiability","author":"Yolcu","year":"2019"},{"key":"2026033012252319800_ref252","first-page":"323","volume-title":"Learning Algorithm Portfolios for Parallel Execution","author":"Yun","year":"2012"},{"key":"2026033012252319800_ref253","first-page":"279","volume-title":"Efficient Conflict Driven Learning in a Boolean Satisfiability Solver","author":"Zhang","year":"2001"}],"container-title":["Foundations and Trends\u00ae in Machine Learning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.emerald.com\/ftmal\/article-pdf\/14\/6\/807\/11134947\/2200000081en.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/www.emerald.com\/ftmal\/article-pdf\/14\/6\/807\/11134947\/2200000081en.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T16:26:31Z","timestamp":1774887991000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.emerald.com\/ftmal\/article\/14\/6\/807\/1331293\/Machine-Learning-for-Automated-Theorem-Proving"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,22]]},"references-count":253,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2021,11,22]]}},"URL":"https:\/\/doi.org\/10.1561\/2200000081","relation":{},"ISSN":["1935-8237","1935-8245"],"issn-type":[{"value":"1935-8237","type":"print"},{"value":"1935-8245","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,11,22]]}}}