KTH / CSC / Teorigruppen / Jakob Nordström / Rekrytering / Doktorandtjänster D-2011-0503

Tjänsterna nedan är tillsatta, och den här webbsidan ligger kvar endast i arkivsyfte.

Doktorandtjänster i teoretisk datavetenskap

Forskargruppen i teoretisk datavetenskap på KTH Datavetenskap och kommunikation (KTH CSC) söker doktorander i teoretisk datavetenskap med inriktning mot beviskomplexitet med kopplingar till SAT-lösning.

Arbetsplatsen

KTH är Sveriges största och äldsta tekniska universitet. KTH svarar för en tredjedel av Sveriges kapacitet av teknisk forskning och ingenjörsutbildning på högskolenivå. Utbildningen och forskningen täcker ett brett område – från naturvetenskap till alla grenar inom tekniken samt arkitektur, industriell ekonomi och samhällsplanering. Totalt finns vid KTH mer än 15 000 studenter på grundnivå och avancerad nivå och över 1 600 forskarstuderande. KTH har nästan 4 300 anställda.

KTH Datavetenskap och kommunikation är en av Sveriges mest framstående forsknings- och undervisningsinstitutioner inom informationsteknologi med verksamhet på både KTH och Stockholms universitet. Verksamheten omfattar utbildning och forskning inom datavetenskapens traditionella kärnområden numerisk analys och datalogi; från teoribildning och analys av matematiska modeller via algoritmutveckling till datorimplementering och simulering. Teknik och metoder för stöd av mänsklig kommunikation och datorstödd samverkan är andra kärnområden av växande betydelse. Den tillämpade forskningen behandlar beräkningsvetenskap, datalogi, datorseende, robotik, neuroinformatik och neurala nätverk, människa-datorinteraktion, medieteknik samt tal- och musikkommunikation. Mer information finns på www.kth.se/csc.

Forskargruppen i teoretisk datavetenskap på KTH CSC (www.csc.kth.se/tcs) erbjuder en stark forskningsmiljö med ett brett spektrum av forskning inom ämnen som till exempel komplexitetsteori och approximationsalgoritmer, data- och nätverkssäkerhet, kryptografi, formella metoder och språkteknologi. Vår forskning publiceras regelbundet i världsledande tidskrifter och konferenser, och gruppens medlemmar har fått ett antal internationella utmärkelser och stora forskningsanslag på senare år.

Arbetsuppgifter

Vi söker doktorander i teoretisk datavetenskap till forskningsprojektet "Understanding the Hardness of Theorem Proving" inom området beviskomplexitet med kopplingar till SAT-lösning.

Att bevisa formler i satslogik är ett problem av stor betydelse såväl teoretiskt som praktiskt. Å ena sidan tror man att det är praktiskt ogörbart att lösa med dator inom rimlig tid i värsta fallet, och att avgöra om det verkligen är så är ett av de berömda Millennieproblemen (P vs. NP). Å andra sidan så används idag s.k. SAT-lösare rutinmässigt för att lösa storskaliga tillämpade probleminstanser med miljontals variabler (samtidigt som man även känner till små formler med bara hundratalet variabler på vilka även de bästa SAT-lösarna går bet).

Inom beviskomplexitet studeras formella system för att resonera om logiska formler. Området har djupa kopplingar till grundläggande frågor inom komplexitetsteori, men motiveras också av kopplingen till SAT-lösning: alla SAT-algoritmer definierar explicit eller implicit ett system i vilket de söker efter bevis, och beviskomplexitet analyserar potentialen och begränsningarna hos sådana bevissystem (och därmed i förlängningen även hos algoritmerna).

Detta projekt syftar till att bryta ny mark inom beviskomplexitet, och till att använda forskningsresultaten för att kasta ljus över frågor relaterade till SAT-lösning. Vi vill förstå vad som gör formler enkla eller svåra i praktiken genom en kombination av teoretiska studier och praktiska experiment, och även belysa andra frågor rörande SAT-lösare som har avgörande praktisk betydelse men där den teoretiska förståelsen är bristfällig. En annan spännande forskningsinriktning är att utforska möjligheten att basera SAT-lösare på starkare bevissystem än vad som används idag. För att göra detta behöver vi dock förstå dessa bevissystem bättre, och här finns en rad välkända öppna problem inom beviskomplexitet som vi vill attackera och lösa.

Projektet leds av Jakob Nordström (www.csc.kth.se/~jakobn) och finansieras av ett Starting Independent Researcher Grant från European Research Council.

Tjänsterna avser fyraåriga tidsbegränsade platser, men kan vid max 20 % institutionstjänstgöring, vanligtvis undervisning, förlängas ytterligare ett år. Forskarstuderande ska vara inskrivna vid KTH. Önskat startdatum är augusti 2012 men är i viss mån förhandlingsbart.

Anställningsform

Anställningsform: Tidsbegränsad anställning
Arbetstid: Heltid
Löneform: Lön enligt avtal för doktorandanställning
Tillträde: Enligt överenskommelse
Antal platser: 2

Kvalifikationer

Lämplig bakgrund för tjänsterna är t.ex. civilingenjörsexamen inom datavetenskap eller teknisk fysik eller masterexamen i matematik. De blivande doktoranderna förväntas ha en stark bakgrund inom och ett brinnande intresse för teoretisk datavetenskap (inom t.ex. komplexitetsteori eller närliggande områden) och matematik (gärna kombinatorik och algebra). Exceptionella kandidater är alltid av intresse oavsett formella förkunskaper. Problemlösningsförmåga och kreativitet är ett måste. Praktisk programmeringsskicklighet är ett stort plus eftersom en del av denna forskning kan komma att handla om att köra storskaliga datorexperiment och utveckla nya programprototyper för SAT-lösning.

Sökande skall vara starkt motiverade för forskarstudier, ha förmåga till självständigt arbete och kritisk analys samt ha god samarbets- och kommunikationsförmåga. Mycket goda kunskaper i att uttrycka sig på engelska i tal och skrift är en förutsättning för att kunna medverka i projektets internationella samarbeten och för att publicera och presentera forskningsresultat i internationella konferenser och tidskrifter.

Ansökan

Sista ansökningsdag: 2012-01-20
Arbetsgivarens referensnummer: D-2011-0503

Ansökningstiden har gå ut, men mycket starka kandidater är fortfarande väkomna att skicka in sina ansökningar. Ansökningarna granskas löpande tills tjänsterna är tillsatta.

Ansökan via e-post skickas till susanneb@csc.kth.se. Skriv in referensnummer på ärenderaden. Ansökan inklusive bilagor ska skickas som PDF-filer.

Ansökan via post skickas till
KTH CSC
Att: Susanne Bergman
Lindstedtsvägen 3, plan 4
100 44 Stockholm

Ansökan skall innefatta följande handlingar:

1. Curriculum vitae.
2. Betygsavskrift från högskola/universitet.
3. Kortfattad redogörelse varför den sökande vill ägna sig åt forskarstudier, inklusive en beskrivning av sökanden med kvalifikationer och intressen.
4. I förekommande fall kopior av sökandens examensarbete och eventuella vetenskapliga publikationer.
5. Namn och adress för tre referenser.

Observera att alla handlingar ovan skall vara på engelska förutom officiella dokument, som även kan vara på svenska.

Som ett led för att förbättra vårt rekryteringsarbete genomför vi en undersökning. Vi vore därför tacksamma om du kunde svara på följande fråga i din ansökan: Var hittade du denna annons? (På vilket svaret är, om du läser detta: på projektledarens webbsidor, eller på den sida från vilken du följde länken hit.)

Upplysningar

Frågor om anställning på KTH besvaras av:
Eva-Lena Åkerman, personalansvarig
Telefon: 08-790 91 06
E-post: ela@csc.kth.se

Frågor om projektet besvaras av:
Jakob Nordström, biträdande lektor
Telefon: 08-790 69 19
E-post: jakobn@csc.kth.se

Fackliga företrädare
Lars Abrahamsson, SACO
Telefon: 08-790 70 58
E-post: lars.abrahamsson@ee.kth.se