[Bath]

Internship on
random satisfiability

Cécile Mailler
Prize Fellow in Probability
James Davenport
Professor in Computer Science

The internship will be based at the University of Bath (UK), co-supervised by Cécile Mailler (Department of Mathematical Sciences) and James Davenport (Department of Computer Science). The internship will focus on the satisfiability problem, and more precisely on a new model of random instances of the satisfiability problem: the so-called “sat-SAT” model. The aims of the internship will be to:

Scientific context

A SAT-solver takes as input a Boolean expression, and gives as output the answer to the question “is this expression satisfiable?” It is known since the work of Cook in 1971 that the satisfiability problem is NP-complete; however, SAT-solvers are surprisingly efficient in practise, suggesting that, although the SAT-solvers have exponential complexity on worst-case inputs, they have polynomial complexity on “typical” inputs.

Models of random SAT inputs are a way to try to understand the structure of typical inputs; the random k-SAT model has been the most famous of these models since the seminal work of Mitchell, Selman, and Levesque in 1997. The reason why the community got excited about this model is because of the phase transition exhibited by Mitchell, Selman, and Levesque, and because the “hard problems lie at the transition”. Proving that the phase transition is sharp is still an open problem despite a lot of efforts from the computer science, probability and statistical physics communities; some of the results obtained in that direction gave new insight in designing faster SAT-solvers (see, for example, Mézard, Parisi, and Zecchina , 2002).

What the student will do

During the internship, the student will study sat-SAT, a new model of random inputs to the satisfiability problem. The main aim is to obtain results similar to the results of Mitchell, Selman, and Levesque, in the context of sat-SAT; we believe that the results of the simulations will be suitable for publication in a computer science conference such as SAT. The student will decide in which programming langage they want to write the code, and will have access to the High Performance Computer of the University of Bath (Balena) to run the simulations.

In parallel to this empirical approach, the student will discuss with Cécile Mailler the theoretical aspects of the project; the main objective of this line of research is to prove that the sat-SAT model exhibits a sharp transition à la 3-SAT. This will be a great opportunity for the student to discover the theory of random trees (in particular about the random binary search tree), although no prerequisites are needed beyond very basic probability. They will also be expected to go through the literature on random 3-SAT in order to understand the bigger picture.

Bath and the University of Bath

The internship will be co-supervise by Cécile Mailler and James Davenport. Cécile Mailler is a member of the Probability group in the Department of Mathematical Sciences, while James Davenport is a member of the Mathematical Foundations of Computing group in the Department of Computer Science. Both groups are very prolific, and each of them run a seminar that the student will be most welcome to attend, depending of their research interests. The student will have regular discussions with both the supervisers all along the project.

Bath is a small but beautiful World Heritage town of the West of England; it is particular famous for its Roman baths, its georgian architecture, and Jane Austeen (see the Wikipedia page for some pictures). The University of Bath is on top of a hill outside of town, the campus is very pleasant, with a library open 24/7, a sports centre (with, in particular an olympic pool), cafés and shops. The walk downtown through the fields offers incredible views of the city. The presence of such a big university make the city of Bath very lively despite its size: the city has two cinemas, one theatre, many pubs, bars, restaurants and clubs. The airport of Bristol is 1:00 hour away by bus, Heathrow 2:00 hours away, London Paddington 1:30 hour and the Eurostar 2:00 hours away.