I skärningspunkten mellan beviskomplexitet och SAT-lösning

Denna föreläsning handlar om en försåtligt enkel fråga: Givet en formel i vanlig satslogik, där variablerna kan ta värdet SANT eller FALSKT, och där de binds samman av logiska operatorer OCH, ELLER och ICKE som anger hur variablerna måste förhålla sig till varandra, kan man snabbt med hjälp av datorberäkningar avgöra om det finns ett sätt att tilldela sanningsvärden till variablerna så att formeln blir satisfierad, dvs. så att alla villkor i den blir uppfyllda?
 
Denna till synes enkla fråga är i själva verket ett av de stora öppna problemen inom teoretisk datavetenskap. Satisfierbarhetsproblemet (SAT) är vad som med fackterminologi kallas NP-fullständigt, vilket indikerar att det förmodligen inte finns effektiva beräkningsmetoder, eller algoritmer, som klarar av alla formler. Att bevisa att så verkligen är fallet verkar dock mycket svårt. Och detta är av stort intresse inte bara inom datavetenskapen -- i samband med millennieskiftet utnämndes problemet av Clay Mathematics Institute till ett av de sju så kallade Millennium Prize Problems som utgör verkligt stora utmaningar inom den moderna matematiken.
 
I skarp kontrast till detta har dramatiska framsteg inom mer tillämpad forskning under de senaste 15-20 åren lett fram till mycket effektiva datorprogram, s.k. SAT-lösare, som kan hantera formler med miljontals variabler. Det saknas dock en djupare teoretisk förståelse varför dessa SAT-lösare är så effektiva och för vilka typer av formler som de fungerar väl.
 
Beviskomplexitet studerar formella metoder för härledning av logiska formler och är ett av få tillgängliga verktyg för teoretisk analys av SAT-lösare. Föredraget kommer att ge en (något selektiv) översikt av beviskomplexitet, med fokus på bevissystem som är av särskilt intresse för tillämpad SAT-lösning, och även diskutera om och hur studiet av sådana bevissystem kan leda till en ökad förståelse av styrkor och svagheter hos moderna SAT-lösare.