The P vs NP question is among the greatest mathematical problems of our time. Surprisingly, in practice it seems to matter little that SAT is NP-hard, and there exist algorithms that solve large instances efficiently. Nevertheless, current algorithms are limited by a theoretical barrier imposed by the resolution proof system. Algorithms that go beyond this barrier should be theoretically stronger, but are less efficient in practice. This is partly because the theory behind these algorithms is less researched.
In this project we will build such theoretical foundations. We will focus on a particular class of algorithms, those implementing the cutting planes proof system, and investigate the reasons currently preventing them from fully implementing cutting planes. We will be working in several areas of computational complexity, primarily proof complexity but also query, circuit, and communication complexity.
A PhD position to work on this project is available starting in 2025. Candidates should have a Masters or Honours degree in mathematics or computer science at the time the position starts. Candidates should have a strong background in theoretical computer science or adjacent areas. Programming ability is desirable but not a requirement.
The position is supported by a Marsden grant. The scholarship covers tuition fees and provides an annual tax free allowance of NZ$34,569 for three years. The successful candidate will be based within the School of Computer Science at the University of Auckland, New Zealand, and supervised by Marc Vinyals. More information on postgraduate studies at the University of Auckland.
To apply, please email your CV, academic transcript, a brief description of your research experience and interests, and names and email addresses of two referees to Marc Vinyals marc.vinyals@auckland.ac.nz. Informal inquiries can be directed to the same address. Applications received by January 20th will be given full consideration. Later applications will be accepted until the position is filled.
Roundingsat is the best certified pseudo-Boolean solver. Help us make it even better! If you are looking for an honours or masters project that combines mathematics, algorithm design, and programming, this may be a good fit. Send an email to marc.vinyals@auckland.ac.nz to know more about it.