Logic List Mailing Archive

PhD student position in "Understanding the hardness of theorem proving", Stockholm (Sweden)

The Theoretical Computer Science group at KTH Royal Institute of 
Technology invites applications for PhD positions in Theoretical Computer 
Science with a focus on proof complexity and connections to SAT solving.

KTH Royal Institute of Technology is the leading technical university in 
Sweden, with education and research spanning from natural sciences to all 
branches of engineering including architecture, industrial management and 
urban planning. The Theoretical Computer Science group at KTH 
(http://www.csc.kth.se/tcs/) offers a strong research environment covering 
a wide range of research topics such as complexity theory and 
approximation algorithms, computer and network security, cryptography, 
formal methods and natural language processing. The group has a consistent 
track record of publishing regularly in the leading theoretical computer 
science conferences and journals worldwide, and the research conducted 
here has attracted numerous international awards and grants in recent 
years.

We are seeking PhD students for the research project "Understanding the 
Hardness of Theorem Proving" in the area of proof complexity with 
connections to SAT solving.

Proving formulas in propositional logic is a problem of immense importance 
both theoretically and practically. On the one hand, this computational 
task is believed to be intractable in general, and deciding whether this 
is so is one of the famous million dollar Millennium Problems (the P vs. 
NP problem). On the other hand, today so-called SAT solvers are routinely 
used to solve large-scale real-world problem instances with millions of 
variables (while there are also small formulas known with just a couple of 
hundreds of variables that cause even state-of-the-art SAT solvers to 
stumble).

Proof complexity studies formal systems for reasoning about logic 
formulas. This field has deep connections to fundamental questions in 
computational complexity, but another important motivation is the 
connection to SAT solving. All SAT solvers explicitly or implicitly define 
a system in which proofs are searched for, and proof complexity can be 
seen to analyse the potential and limitations of such proof systems (and 
thereby of the algorithms using them).

This project aims to advance the frontiers of proof complexity, and to 
leverage this research to shed light on questions related to SAT solving. 
The project is led by Jakob Nordstrom (http://www.csc.kth.se/~jakobn) and 
is financed by a Starting Independent Researcher Grant from the European 
Research Council.

These are full-time positions, normally for five years including 20% 
teaching, with salary according to KTH PhD student regulations 
(internationally very competitive). The successful candidates are expected 
to start in August 2012, although this is to some extent negotiable.

The application deadline is January 20, 2012 but candidates are encouraged 
to apply already now. See 
http://www.csc.kth.se/~jakobn/openings/D-2011-0503-Eng.php for the full, 
formal announcement with more information. Informal enquiries about these 
positions are welcome and may be sent to Jakob Nordstrom.