As of April 2000, PhD studentships at St Andrews University are available.
Currently proposed projects are all in the general area of combinatorial search problems in Artificial Intelligence, and are as follows:
QSAT is a Quantified version of the SATisfiability problem. Satisfiability is a classic intractable problem and has become very important in Artificial Intelligence. QSAT (also known as QBF for Quantified Boolean Formulae) is a richer version of the problem, and has possible applications in domains such as planning. It is more expressive than SAT but harder to solve. Technically, while SAT is NP-complete, QSAT is PSPACE-complete. This puts QSAT into the same complexity class as games like Go. While there are algorithms to solve QSAT, there is a need for further investigation and the possibility of inventing improved algorithms, as well as developing applications of QSAT. The close link between QSAT and games should be exploited, integrating techniques from AI research into games and search problems.
What makes a problem hard to solve? One of the most important reasons is criticality. If a problem is critically constrained, it is hard to tell if it has a solution or not. Recently, we have made significant advances in understanding criticality in domains such as graph coloring and satisfiability, and for two very different kinds of algorithm. This research has been helped by exciting new links with physics. There are many avenues for exploring this work, one of the most important being the application to real problems as well as the purely random problems that have been most studied so far.
Constraint programming is a successful technology for applying modern
AI search algorithms to real world problems. One limitation is that many
real world problems contain high degrees of symmetry. In scheduling a tournament
for example, all the players might be interchangeable. This leads to great
redundancy and inefficiency in search. We have recently developed constraint
programming techniques to address this problem, and demonstrated their
effectiveness. The proposed research is to integrate our new methods with
algebraic systems such as GAP for more efficient handling of symmetries.
The result should be greatly improved symmetry breaking techniques and
a demonstration of the applicability of GAP.
Combinatorial search for problems such as satisfiability is highly processor intensive. It is therefore natural to wish to use parallel processing to get results faster. Parallelising search is non-trivial, especially for algorithms which communicate between different parts of the search space, such as backjumping and learning algorithms. We have recently provided what we believe to be the first parallel implementation of Conflict Directed Backjumping. As well as being interesting in its own right, implementing search in parallel functional languages provides an excellent and practical application for testing functional programming languagues. At St Andrews we have a Beowulf cluster and so are well placed to carry out this research.
How do we know our programs are correct? One answer is to use the beautiful link between proofs and programs to derive correct programs. Indeed, it is even possible to extract programs automatically from proofs, and this has been made much more practicable by recent work by Jim Caldwell. Using this, we have been able to extract a correct program for the important search algorithm Conflict Directed Backjumping for problems like satisfiability and Hamiltonian circuit. We propose to extend this research to further algorithms and, especially, more complex problems such as Intuitionistic Propositional Logic and QSAT.