Open Positions

Postdoc Positions

I currently have no funding for more postdocs, but in case it can be of interest there is one other option I know of for postdoc positions with other sources of funding.

Namely, there are postdoctoral scholarships from the Wenner-Gren Foundations [information in Swedish only], where the deadline is October 1, 2012 for positions starting in January 2013 at the earliest. In this case, formally the host is the one submitting the application. You should not have spent more than nine month in Sweden prior to the application, and your PhD degree should be no more than five years old (but if it is, there is the possibility to apply for somewhat more limited funding in terms of visiting researcher scholarships [again the info is in Swedish]).

I would be willing to consider submitting a (jointly produced) application for an additional postdoc working on research somehow related to my project on proof complexity and SAT solving. If you think this could be of interest for you, you are welcome to send me an e-mail so that we can discuss this further.

PhD Positions

I currently have no funding for more PhD students, but in case it can be of interest there are two other options I am aware of for PhD studies at KTH with other sources of funding.

For Chinese students, KTH is a partner of the China Scholarship Council and receives quite a few students yearly with funding via this program. Open positions are usually announced in the autumn and applications should be submitted during the winter.

For Brazilian students, it might be possible to get funding for parts or all of a PhD at KTH from the Science Without Borders program, where KTH is also a partner university.

I would be willing to consider additional PhD students in my project on proof complexity and SAT solving. If you think this could be of interest for you, you are welcome to send me an e-mail so that we can discuss this further.

Master's Thesis Projects

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.

Formula Hardness and SAT Solving

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).