Om effektiva bevis för lösbara problem  

Docent Jakob Nordström får anslag av Knut och Alice Wallenbergs Stiftelse, till en postdoktoral tjänst för att rekrytera en forskare från utlandet till Skolan för datavetenskap och kommunikation, KTH, Stockholm. 

Om det går att med ett dataprogram snabbt bekräfta en lösning till ett matematiskt problem, går det då även att finna en algoritm som snabbt ska kunna lösa problemet? Frågan är nära besläktad med det viktigaste problemet inom den teoretiska datavetenskapen, känt som P=NP?.  

Exempelvis kan en dator snabbt kolla lösningen till frågan om det inom en mängd heltal, som 3, 8, 13, 14 och 16, finns en delmängd som ger summan 25. Svaret är ja, eftersom 3+8+14=25. Även om mängden heltal är väldigt stor, går det att med hjälp av en dator att snabbt bekräfta resultatet. Men det finns ingen algoritm som kan ge lösningen inom rimlig tid.  

Att P är lika med NP innebär att det är möjligt att skapa en sådan snabb algoritm. Många matematiker tror dock att P inte är lika med NP, alltså att det finns problem av denna typ som inte går att lösa på en dator inom överskådlig tid. Ingen har dock ännu kunnat bevisa det.  Den som först kommer med svaret belönas med en miljon dollar från Clay Mathematics Institute som år 2000 instiftade priset för att lösa något av de sju mest centrala problemen för det kommande milleniet. 

Problemet P=NP? har gett upphov till ett nytt forskningsfält kallat beviskomplexitet. Det finns flera skäl till att ägna sig åt beviskomplexitet. Ett är att studier av formella metoder, bevissystem, kan leda till en lösning på P=NP? problemet. Ett annat är att denna forskning kan leda till utveckling av metoder att mäta hur djupa olika matematiska sanningar är. Med detta menas att det blir möjligt att bestämma hur kraftfulla bevissystem som krävs för att visa att familjer av redan kända påståenden är sanna.  

Beviskomplexitet är också ett av de få verktyg som kan användas för att utforska så kallade SAT-lösare. Dessa är datorprogram som används framgångsrikt inom många skilda tillämpningar, som hårdvaru- och mjukvaruverifiering, artificiell intelligens, kryptografi, bioinformatik och till och med ren matematik. Planen är att inom projektet fördjupa förståelsen för styrkor och svagheter hos olika bevissystem.