Start February 2025
Research themes related to the topic Machine Learning, Reinforcement Learning, SAT, Logic, Constraint Programming, Trustworthy AI
Location: LaBRI, Bordeaux Computer Science Research Laboratory, Talence, France
(This Master’s internship is funded by the “Trustworthy AI” chair, led by Laurent Simon and supported by the Bordeaux University Foundation)
Description of the proposed master’s project
Machine Learning (ML) is probably the field of Artificial Intelligence (AI) that has most contributed to the progress observed in AI in recent years, renewing strong enthusiasm for this field, which began more than 65 years ago. These impressive results are due to multiple factors. In addition to a better understanding of the strengths and weaknesses of learning algorithms, the ML ecosystem has massively turned towards the production of powerful and open tools, exploiting the latest hardware advancements in the best possible conditions. Even better, the hardware has evolved, especially for tasks known as Deep Learning (DL), and specialized machines or dedicated computing cards have appeared, allowing learning on gigantic data volumes. The accessibility of large computing clusters has also made it possible to consider learning techniques that allow learning new strategies. These techniques, grouped under the general principles of Reinforcement Learning (RL), only consider the allowed actions, the possible states of a given system, and the relationships between them. Then, guided by a specific reward function, the system learns, by itself, the actions to undertake to maximize the expected rewards from any initial state. The progress made in RL is also remarkable in many fields. For example, Alphago, even though it integrates more classical game tree exploration algorithms that are not learned, is probably the most striking example of the extent of the progress observed in the field.
However, despite these stunning results (even earning a Nobel Prize in Chemistry), ML/RL-based approaches have not yet succeeded in surpassing conventional methods in solving NP-Hard problems. This class of problems, at the heart of theoretical computer science, captures the difficulty of many AI subdomains since its inception, such as planning, constraint programming, or even the SAT problem itself (SAT stands for “Satisfiability Testing”).
While the ML field can be described as “statistical” AI (approaches can often be reduced to finding correlations in observed events), the SAT field is at the heart of many “symbolic” AI approaches. Its “symbolic” nature comes from the fact that this problem mainly relies on manipulating logical symbols with precise semantics.
The objective of this Master 2 internship is to study how recent advances in ML/RL can allow us to consider the use and extension of ML/RL techniques for the practical resolution of the SAT problem.
The SAT problem is based on propositional logic, which allows it to be at the heart of a whole class of equivalent (in difficulty) AI problems, as long as they are based on logical reasoning. Seemingly extremely simple, this logic perfectly adapts to the brute computational power of current machines, while offering a range of pragmatic solutions to a whole set of fundamental Artificial Intelligence (AI) problems. Research on the practical resolution of SAT is particularly active. Thus, each year, the community organizes competitions to evaluate progress and challenges. Up to forty teams can participate, involving more than fifty demonstrators in the competitions. One of the main research paradigms around SAT is to rely on the computational speed of machines to allow them to very quickly explore the solution search space. This involves deploying extremely fast decision heuristics, allowing solvers to make hundreds of thousands of decisions per second.
It is therefore natural to challenge this paradigm by allowing solvers to rely on slower but more intelligent decisions through the application of ML/RL methods to solve the problem.
Behind this seemingly natural idea, however, lies a number of very difficult problems, and taking on this challenge means tackling difficulties at the intersection of RL/ML and SAT foundations.
The approach we propose to study in this internship seeks to improve local search through a more or less direct modeling of SAT problems in RNN (for example, based on graph neural networks (GNN [1,2])). This method should allow changing the paradigm of local search SAT solvers (LS), which is based on extremely fast solvers, taking almost no time for decisions (each decision flips the value of a variable, hoping to reach a solution or get closer to it). Unfortunately, this approach faces several problems. (1) Each family of SAT problems has its own characteristics, limiting the generalization capabilities of RL methods. (2) The inference times of NN predictions are much too slow to correct their inaccuracies. (3) The size of the instances to be processed can vary significantly (from a few hundred variables to millions), making the fixed modeling generally used in RL methods quite difficult to implement. (4) SAT problems cannot be approached locally, limiting the use of GNNs. These points were identified in [5] to explain the reasons for the relative failure of these methods in the context of SAT. The difficulty encountered is not surprising: finding a smarter way to navigate the solution landscape through local search has been a major challenge for the community for years. It is actually challenge 6, almost 30 years ago, proposed by B. Selman, H. Kautz, and D. Mc Allister, in “Ten Challenges in Propositional Reasoning and Search” (IJCAI’97): Improve stochastic local search on structured problems by effectively handling semantic dependencies between variables. This challenge has never been successfully met. So far, with rare exceptions, local search has remained confined to random problems, for which the solution landscape was well known.
Proposing a model, possibly guided by the model learned by the RL engine, in the context of industrial SAT problems is therefore a formidable challenge that we propose to study in this Master internship.
Bibliography
[1] How Powerful are Graph Neural Networks?, K. Xu, W. Hu, J. Leskovec, S. Jegelka, in Seventh International Conference on Learning Representations (ICLR, 2019)
[2] Learning Local Search Heuristics for Boolean Satisfiability, Emre Yolcu, Barnabas Poczos, NeurIPS 2019
[3] NeuroSAT: Learning a SAT Solver from Single-Bit Supervision, Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, David L. Dill (arxiv)
[4] Guiding High-Performance SAT Solvers with Unsat-Core Predictions, Daniel Selsam, Nikolaj Bjorner (arxiv)
[5] Can Q-Learning with Graph Networks Learn a Generalizable Branching Heuristic for a SAT Solver? Kurin, Vitaly and Godil, Saad and Whiteson, Shimon and Catanzaro, Bryan, NeurIPS 2020
[6] On the Non-degeneracy of Unsatisfiability Proof Graphs Produced by SAT Solvers, Rohan Fossé, L. Simon, CP 2018
[7] The Glucose SAT Solver, Gilles Audemard, Laurent Simon, IJAIT’s Volume No.27, Issue No. 01.2018
Candidate
The candidate should have solid knowledge in Machine Learning and symbolic AI. Very good programming skills are also expected.
Contact: Laurent Simon