Ansökan: Effektiv Hantering av Kvantifierare i SMT-Lösare

Tidsperiod:

1 januari 2015 – 31 december 2018

Projektledare:

Philipp Ruemmer

Finansiär:

Vetenskapsrådet

Bidragstyp:

Projektbidrag

Budget:

3 840 000 SEK

Villkorslösare är ett viktigt hjälpmedel inom många olika IT-områden, t.ex. för verktyg att analysera och verifiera programvaror, generering av testfall, schemaläggning av arbete, operationsanalys eller datorassisterad resonerande kring matematiska påståenden. Inom alla dessa områden är det nödvändigt att lösa stora och komplicerade sökproblem, t.ex. för att schemalägga personal på ett sjukhus.

För att lösa ett sådant problem behöver man ställa upp alla villkor som måste uppfyllas, t.ex. "ett arbetspass är åtta timmar", "en anställd jobbar 40 timmar under en vecka", "en avdelning behöver åtta personer på plats", o.s.v. Dessa formuleras som matematiska formler som en villkorslösare sedan försöker hitta en lösning till; varje sådan lösning representerar ett arbetschema som uppfyller alla villkor.

De senaste åren har villkorslösare utvecklats som är oerhört effektiva på att lösa stora formler med upp till flera miljoner variabler och villkor. SMT (Satisfiability Modulo Theories) är en modern arkitektur för att bygga villkorslösare. Det är en påbyggnad av SAT-lösare (boolean SATisfiability), där man utökat funktionaliteten genom att inte bara ta formlerna i beaktande, utan även bakomliggande teorier såsom aritmetik eller funktioner. SMT-lösare har blivit mycket framgångsrika under de senaste åren, och har inom många områden lett till nya algoritmer och lösningar för hitintills svåra problem.

Vissa villkor kan dock vara svårare att hantera än andra, särskilt villkor som ska uppfyllas "för alla" eller "för vissa" värden (t.ex. "Det måste finnas ett schema för alla möjliga beläggningar på en avdelning"). Sådana villkor uttrycks ofta med hjälp av kvantifierare och är en utmaning för dagens lösare. De flesta SMT-lösare kan i grund och botten inte hantera kvantifierare, utan använder sig av heuristiker att instansiera formler som innehåller kvantifierare, tills alla möjligheter är uttömda; denna metod är tidskrävande och fungerar inte för alla formler. Andra lösare för formler inom första ordningens logik kan hantera kvantifierare på ett effektivt sätt, men stöder inte att ta teorier, såsom aritmetik, i beaktande.

På grund av detta har en effektiv hantering av både teorier och kvantifierare tillsammans blivit identifierad som en av de huvudsakliga utmaningarna under utvecklingen av lösare. Det här projektet syftar till att lyfta SMT-paradigmen till första ordningens logik genom att inkludera kvantifierare som första klassens "medborgare" i lösare. Detta kommer att möjliggöra effektivare beräkningar med villkor som innehåller både teorier och kvantifierare.

Målet är att designa ett nytt ramverk för SMT med ett systematiskt och effektivt stöd för kvantifierare genom att kombinera teknik från SMT tillsammans med metoder i första ordningens logik. Det nya ramverket kommer att kunna hantera olika teorier och implementeras på ett modulärt sätt, som är de-facto standard i dagens SMT-lösare, med målet att uppnå samma prestanda som SMT-lösare. Samtidigt kommer det nya ramverket att kunna hantera mer komplicerade villkor än existerande lösare, som har stor betydelse i en mängd olika domäner, bl.a. verifiering av mjukvara, analys av hybrida eller cyberfysiska system såväl som i datorassisterat matematikresonemang. Det kommer också att undersökas hur så kallade Craig interpolanter kan genereras utifrån villkor eller formler inom det nya ramverket; Craig interpolanter har visat sig vara ett viktigt verktyg inom verifiering de senaste åren.