I am looking for postdocs in computational complexity and also in SAT solving with an intended starting date of August-September 2017. These are fully funded positions (including travel money) with an internationally competitive salary. The application deadline is March 31, 2017. Please feel free to drop me a line if you have any questions.
If you instead want to start collecting grants to list on your CV, you can also try to apply for an Individual Fellowship within the EU Marie Skłodowska-Curie actions program to come and do a postdoc with me (as soon as they have an open call — last time was in September 2016). I would particularly welcome applications from strong candidates who want to work at the intersection of proof complexity and applied SAT solving. Please feel free to contact me if you want to discuss this.
I am looking for PhD students in computational complexity theory (together with Johan Håstad and Per Austrin) and also in SAT solving with a starting date of August-September 2017. This are fully funded positions with an internationally very competitive salary. The deadline for applications is March 31, 2017. Feel free to drop me a line if you have any questions.
I would be interested in supervising one or several Master's students for thesis work within the framework of the research project briefly outlined below. Please do not hesitate to send me an e-mail to get more detailed information. (Note, however, that these projects are intended for students registered at KTH or who are geographically close and can work on their thesis here at KTH. There is no separate funding available to support foreign students to come to Sweden.)
Given a logic formula, is it possible to set its variables in such a way that the formula is satisfied? This simple looking problem has been on centre stage in theoretical computer science ever since the field got started some 40 years ago, and was recently named as one of the Millennium Prize Problems comprising some of the major challenges for all of mathematics in the 21st century. Today, students of computer science worldwide learn in their introductory theory courses that this so-called SAT problem is what is known as NP-complete, and therefore is very, very hard in practice.
Interestingly, practioners take a somewhat different view. During the last 10-15 years, SAT has developed from a problem of mainly theoretical interest into a practical approach for solving applied problems. Enormous progress in performance has led to satisfiability algorithms, so-called SAT solvers, becoming a standard tool for solving real-world problems with millions of variables in the context of, for example, hardware and software verification, electronic design automation, artificial intelligence, operations research, and bioinformatics. The theory of NP-completeness did not quite go away, however — for all these SAT solvers there are also known examples of tiny formulas with just a couple of hundred variables that make them fail miserably.
How can modern SAT solvers be so good in practice? And how can one know for a particular formula whether it will be hard or easy? These are the kind of questions we want to study in these Master's thesis projects, using a mix of theoretical research and practical experiments.
The projects are intended to give students a feel for what research in theoretical computer science is like, while at the same time focusing on concrete problems of practical importance. Apart from the Master's thesis itself, the intention is that the results will also be published as (parts of) papers in leading scientific conferences and/or journals in the field (in the framework of the research outlined here).