Doktorand i teoretisk datavetenskap Job in Stockholm 10044, Stockholm Sweden
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 15000 studenter på grundnivå och avancerad nivå och över 1600 forskarstuderande. KTH har nästan 4300 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 med 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 om CSC finns på www.kth.se/csc .
Forskargruppen i teoretisk datavetenskap (www.csc.kth.se/tcs) på CSC 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. Som kontrast till detta känner man även till små formler med bara hundratalet variabler på vilka 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 även 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änsten avser en fyraårig tidsbegränsad plats, men kan vid max 20 % institutionstjänstgöring, vanligtvis undervisning, förlängas ytterligare ett år. Forskarstuderande ska vara inskriven vid KTH.
KVALIFIKATIONER
Lämplig bakgrund för tjänsten är t.ex. civilingenjörsexamen inom datavetenskap eller teknisk fysik eller masterexamen i matematik. Den blivande doktoranden 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ökanden skall vara starkt motiverad 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.
ANSTÄLLNINGENS OMFATTNING
Anställningsform: Tidsbegränsad anställning, tillträde: Önskat startdatum är augusti 2012 men är i viss mån förhandlingsbart.
Omfattning: Heltid.
ANSÖKAN
Ansök senast: 2012-01-20
Referensnummer: D-2011-0503
Du kan söka detta jobb genom:
Via e-post: Susanne Bergman susanneb@csc.kth.se
Via post: KTH/CSC Att: Susanne Bergman, Lindstedtsvägen 3 100 44 Stockholm
LÖN
Lön enligt KTHs doktorandstege.
ANSTÄLLNING
Antal annonserade arbetstillfällen: 2 plats(er)
KONTAKTPERSONER
Eva-Lena Åkerman
personalansvarig
08-790 91 06
ela@csc.kth.se
Jakob Nordström
Bitr Universitetslektor
08-790 69 19
jakobn@kth.se
Lars Abrahamsson (facklig)
SACO
08-790 70 58
lars.abrahamsson@ee.kth.se
ÖVRIGT
Vid ansökan via e-post skriv in referensnummer i ärenderutan. Ansökan inklusive bilagor skickas i pdf-format. Ansökan via post skriv ärendenummer på kuvertet.
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.
www.kth.se