Potential 3rd and 4th Year or Masters Projects
My research interests are primarily mathematical, typically involving formal logic, category theory and the foundations of computer science. If you are interested in a mathematical project in these areas, please contact me directly.
Although my work is theoretical, I have over a decade of industry software development experience, and am happy to supervise programming projects. I suggest a few potential directions below, although I am open to discussing variations or similar projects. Students should be enthusiastic about coding, and producing a good quality software implementation. Only limited knowledge of the background mathematics should be required, and can be explored to the taste of the students involved.
All the projects are intended to be challenging, and therefore offering the scope for an impressive project assuming enough time and effort is invested.
Games and SAT Solvers
The propositional satisfiability problem is the canonical example of an NP-complete problem. Generalising propositional logic leads to more expressive logics such as quantified Boolean logic (QBF), dependency quantified Boolean logic (DQBF), second order quantified Boolean logic (SOQBF), modal logic and the mu-calculus, each of which yields complete problems for well-known complexity classes. Many of these logics have available solvers that can be used to explore the practicalities of their satisfiability problem.
Another source of complete problems for complexity classes is to consider the problem of finding winning strategies for certain games and puzzles. The starting point for this project would be to explore this relationship from a practical point of view. Can appropriately chosen standard satisfiability solvers provide useful tools for finding winning strategies for games and puzzles? How well does this scale? What are the choices when encoding games as satisfiability problems?
This project might suit students with interests in either AI, logic or algorithms, with the direction taken adjusted to their interests.
Generic Game Solver
As well as being educational and fun to play, games are a flexible abstraction for describing different types of interaction and decision making. Many problems in computer science can naturally be phrased as a requirement for a winning strategy for a suitable game. The aim of this project would be to develop software that finds winning strategies for a general class of games. Aspects of the project could include:
- Identifying a general class of games that has concrete games of interest as special cases.
- Implementing one or more solution strategies for finding winning strategies.
- Evaluating the scalability of the game solver as a general purpose problem solving tool.
- Considering how to certify that a winning strategy has been found that can be validated independently.
The project would be suitable for students with interests in algorithm design or artificial intelligence.
A Turing Machine Compiler
Turing machines crop up in many parts of theoretical computer science. In some applications, such as the study of busy beaver numbers, it is useful to have a concrete Turing machine implementing a given program. See for example this paper showing that sufficiently big busy beaver numbers are, very loosely speaking, “outside the scope of formal mathematics”.
The aim of this project is to produce a compiler for a simple programming language, generating Turing machines as the target output. As a supporting goal, it will be necessary to implement a Turing machine simulator to run the output of the compiler. A stretch goal would be to optimise the number of states of the generated Turing machines, as this is of interest in applications.
This is primarily a programming project, but with some challenging design questions to address. It would suit a student interested in some combination of compilers, programmings languages and theory of computation.
A Guarded Fixed Point Logic SAT Solver
Guarded logic is a very expressive logic, greatly generalising modal logic. Guarded fixed point logic (GFP) further extends guarded logic with fixed point connectives, encompassing the expressive power of many temporal logics. Despite this expressive power GFP is decidable – that is, we can systematically decide if a sentence can be made true. This has many applications, such as in software verification and AI.
The aim of this project is to implement a SAT solver for GFP. This will be challenging as the decision procedure is complex, and only appears in academic papers. This project would suit a student with strong programming skills, and the persistence to extract the details of the algorithm from the literature, aided by support from your supervisor.
A Bernays-Schönfinkel-Ramsey Class SAT Solver
The Bernays-Schönfinkel-Ramsey class is a decidable fragment of first-order logic, and is in fact NExpTime complete. The complexity of the satisfiability problem implies we will not be able to solve this problem efficiently in general, but does not preclude satisfactory performance on instances that might be of practical interest. The aim of this project is to implement and evaluate a satisfiability solver for this logic.
This project would suit a student with strong programming skills in a “fast” language such as C++ or Rust, although an implementation using a less obvious language could be considered.
Exploring the Weisfeiler-Leman algorithm
Colour refinement, and its generalisation the Weisfeiler-Leman algorithm are algorithms with connections to many areas including logic, linear programming, machine learning and the famous graph isomorphism problem. Intuitively these algorithms iteratively colour subsets of vertices of a graph as they extract more information about the relationships between different sets of vertices. There are several variations of this algorithm for different graph types such as directed or weighted graphs.
The aim of this project would be to explore programmatic aspects of variations of the Weisfeiler-Leman algorithm. This could be done in many ways, such exploring efficient implemenations of these algorithms, or visualisers of their behaviour.
Implementing an Automata Programming Library
Students often encounter finite state automata in introductory courses on models of computation, such as Nottinghams Languages and Computation course. There are many generalisations of this notion, such as automata that run on infinite words and trees. These more general automata are important in advanced algorithms and decision procedures.
The aim of this project would be to implement a software library support these more advanced notions of automata, and manipulations that are commonly performed on them. The aim should be for an elegant, efficient and extensible library using modern programming techniques, suitable for use in realistic applications. Ideally this would be in a popular “efficient” language such as C++ or Rust, although other choices such as Haskell would also be interesting.
This project would suit a student with strong programming skills, and an interest in exploring automata beyond the introductory level.
Games from formal logic
There are a multitude of games associated with formal logic, such as model comparison games, semantic games and model construction games. There are many potential programming projects involving these games, such as developing solvers that establish winning strategies for one of the players.
Games on graphs
Similarly to the situation in logic, there are a vast number of games that can be played on graphs and graph like structures. Examples include pursuit evasion games such as cops and robbers, and graph theoretic variants of combinatorial games such as Nim. These games have many uses in mathematics and computer science, such as to study and quantify the combinatorial structure of graphs, or in connection with important algorithmic problems. Again, there are a variety of different directions a programming project could go in, such as automated solvers or AI techniques for playing these games.
Dan Marsden 