Machine Learning for SAT search

Most recent news

(list of all news)

Glucose is (finally) on Github

(17 May 2023)

Glucose is finally (also) distributed on Github. The idea is simply to allow official forks from Glucose versions. We used to distribute it only via the archives and the official...


Interview in the Regional Newspaper "Sud-Ouest" about Trustworthy AI

(03 May 2023)

A.I. has been the subject of many, many press articles in recent months. The exposure of tools such as chatGPT4 to the general public accelerates even more the need for...


Invitation to the Simons Institute (Berkeley)

(17 April 2023)

As part of the Simons Institute’s SAT Program (SAT Reunion Semester), I had the pleasure of being invited for a long stay in this famous research place about theoretical computer...


Lauch of the DIHNAMIC European Project

(20 March 2023)

The Dihnamic project has just been launched very officially. It is a large-scale European and regional project in which I act as a member of the advisory board. The project...


Dataquitaine 2023

(02 March 2023)

The sixth “Dataquitaine” (a regional scientific event organized in Nouvelle-Aquitaine) days were held on Thursday 2 March 2023 at Kedge Business School, organised by Digital Aquitaine and especially the Domex...

Master’s Research Internship in Artificial Intelligence (+ PhD)

Starting Feb. 2023

Disciplinary fields related to AI: Machine Learning, Reinforcement Learning, SAT, Logic, Constraint Programming, Trustworthy AI

Localization: LaBRI, Laboratoire Bordelais de Recherche en Informatique, Talence, France

(This Master’s Internship will be fully funded by the chair “towards a trustworthy A.I.” led by Laurent Simon and supported by the Fondation Bordeaux Université)

The topic is currently associated with a funding for a PhD that is beeing set up thanks to a CIFRE mechanism

Research Project Description

Machine learning (ML) is certainly the field of artificial intelligence (AI) that has contributed the most to the progress observed in AI in recent years, renewing a strong enthusiasm in this field, born more than 65 years ago. These impressive achievements are due to multiple factors. In addition to a better knowledge of the strengths and weaknesses of learning algorithms. The ML ecosystem has turned massively towards the production of powerful and open tools, exploiting in the best possible conditions the latest advances in the material made available, by the most powerful firms that have ever been created (Google, Microsoft, Tesla, Microsoft, Amazon, NVidia, Intel,…). Even better, the equipment has evolved especially for so-called Deep Learning (DL) tasks and specialized machines, or dedicated calculation cards, have emerged, allowing learning on gigantic volumes of data. The accessibility of large computing clusters also made it possible to consider learning techniques that gradually discovered what had to be learned. These techniques, grouped under the general principles of Reinforcement Learning (RL), consider only the authorized actions, the possible states of a given system and the relationships between them. Then, guided by a specific reward function, the system learns, on its own, the actions to be taken to maximize the rewards expected from any initial state. Progress in RL is also remarkable in many areas. For example, Alphago, even if it incorporates more classical game tree exploration algorithms, which is not learned, is probably the most striking example of how far progress has been observed in the field.

However, despite these breathtaking results in pattern recognition and signal analysis (sound, image, video, ….) and text, ML / RL-based approaches have not yet succeeded in overtaking conventional methods in solving NP-Hard problems. This class of problems, at the center of theoretical computer science, captures the hardness of a many subfields of AI since its beginnings, such as planning, constraints programming, or even the SAT problem itself (SAT is for “Satisfiability testing”, the main goal of which is precisely to tackle this central problem).

If the ML domain can sometimes be qualified as “Statistical” AI, because the approaches can often be reduced to finding correlations in observed events, the SAT domain is at the heart of many “Symbolic” AI approaches. Its “Symbolic” nature comes from the fact that this problem relies mainly on the manipulation of logical symbols equipped with precise semantics.

The goal of this Master Internship is to study how recent progress in ML / RL may allow us to consider the use and the 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 AI problems, as soon as they are based on logical reasoning. Extremely simple, this logic fits perfectly with the raw computational force of current machines, while offering a panel of pragmatic solutions to a whole set of fundamental Artificial Intelligence (AI) problems. Its apparent simplicity allows the development of compact and efficient algorithms - in practice - to attack a whole class of important problems, but intractable - in theory -. Edmund Clarke, one of the 2007 Turing Award winners (and user of SAT demonstrators) said “the practical resolution of the SAT problem is a key technology for 21st century computing”. D. Knuth, in his booklet on SAT, wrote “The story of satisfiability is the tale of a triumph of software engineering, blended with rich doses of beautiful mathematics. Thanks to elegant new data structures and other techniques, modern SAT solvers are able to deal routinely with practical problems that involve many thousands of variables, although such problems were regarded as hopeless just a few years ago.”. It is also important to point out that research into the practical resolution of SAT is particularly active. Each year, therefore, the community organizes competitions to assess progress and challenges. Up to forty teams can participate, involving more than fifty demonstrators in competitions. One of the important research paradigms around SAT is to rely on the computation speed of machines to enable them to travel extremely quickly through the search space for solutions. This involves the deployment of 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 smarter decisions thanks to the application of ML / RL methods for solving the problem.

Behind this seemingly natural idea, however, hides a number of very difficult issues, and tackling this challenge means having to make a significant contribution to the foundations of RL/ML as well as to the best SAT algorithms.

The approach we propose to study in this internship seeks to improve local search thanks to a more or less direct modeling of SAT problems in NN (for example based on neural networks on graphs (GNN [1,2])). This method should make it possible to change the paradigm of local search (LS) SAT solvers, which is based on extremely fast solvers, taking almost no time for decisions (each decision inverts the value of a variable, in the hope to reach a solution, or to come closer to it). Unfortunately, this approach faces various problems. (1) each SAT problem family has its own characteristics, which limits the generalization capacities of RL methods. (2) the inference times of the NN predictions are far too slow to correct their inaccuracies. (3) the size of the instances to be processed can vary significantly (ranging from several hundred variables to millions), which makes the fixed modelizations typically used in RL methods quite difficult. (4) SAT problems cannot be approached locally, which limits the use of GNNs. These points were identified in [5] to explain the reasons for the relative failure of these methods in the SAT framework. The difficulty encountered is not surprising: finding a smarter way to navigate the solutions landscape through local search has been a significant challenge for the community for years. This is in fact challenge 6, almost 25 years ago, proposed by B. Selman, H. Kautz and D. Mc Allister, in “Ten Challenges in Propositional Reasoning and Search” (IJCAI’97): Improving local search stochastic on structured problems by effectively dealing with semantic dependencies between variables. This challenge has never been successfully met. Until now, with rare exceptions, local search has remained confined to random problems, for which the solution landscape was well known.

Getting to propose a model, possibly guided by the learned model by the RL engine, in the context of industrial SAT problems is therefore a formidable challenge that we propose to study in this Master’s Internship.

Short 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 an excellent scientific background and a good knowledge of logic-based reasoning methods. In addition, a very good level of programming is also expected.

The internship can start as early as February 2023.

Contact: Laurent Simon