Satisfierbarhet modulo teorier

Satisfierbarhet modulo teorier (SMT) är en formaliserad utökning av logiska formler inom datavetenskap och matematisk logik. Ett SMT-problem uppkommer genom att man kombinerar första ordningens logik och likhet med relationer mellan symboler, där tolkningen av både relationerna och symbolerna är godtyckliga och definieras av den logiska teori de tillhör. Exempel på teorier som ofta används inom datavetenskap är teorierna om reella tal och om heltal, som kan användas till exempel för att uttrycka ekvationer över tal med okända variabler (). Själva problemet SMT handlar om att ge en tilldelning till dessa symboler så att alla villkor är uppfyllda. På det sättet kan SMT  beskrivas som en av flera formaliseringar av villkorsprogrammering.

Mer specialiserade teorier är de om olika datastrukturer såsom listor, matriser, bitvektorer, strängar och så vidare.

Grundläggande terminologi 
Formellt sett är en SMT-instans en formel i första ordningens logik, där vissa funktions- och predikatsymboler har ytterligare tolkningar. SMT-problemet är att avgöra om en sådan formel är satisfierbar, det vill säga har en möjlig tilldelning av alla variabler så att alla villkor är uppfyllda. Ett SMT-problem kan också beskrivas som en utökning av boolesk satisfierbarhet (SAT) där vissa av de binära variablerna ersätts av predikat över en lämplig uppsättning icke-binära variabler.

Ett predikat är en binärvärderad (sann eller falsk) funktion av icke-binära variabler. Exempel på predikat inkluderar linjära olikheter (t.ex. ) eller likheter som inbegriper otolkade termer och funktionssymboler, t.ex. där är en ospecificerad funktion av två argument.

Den semantiska meningen hos varje predikat definieras av dess teori. Till exempel utvärderas linjära olikheter över reella variabler med hjälp av reglerna för teorin om linjär reell aritmetik, medan predikat som involverar otolkade termer och funktionssymboler utvärderas med hjälp av reglerna för teorin om otolkade funktioner med likhet (ibland kallad den tomma teorin). Andra teorier inkluderar teorier om matriser och liststrukturer (används ofta för att modellera och verifiera datorprogram) och teorin om bitvektorer (vanliga vid verifiering av hårdvarudesign och för att representera heltal av känd bredd). På senare tid har teorin om strängar, en formalisering av strängvillkor, blivit viktig inom verifiering av webbapplikationer och andra program som manipulerar text.

Lösare 
Ett program som avgör (och vanligen också hittar en lösning till-) en instans av ett SMT-problem kallas för en SMT-lösare.

Standardisering och SMT-COMP-tävlingen 
Det finns flera standardiserade gränssnitt för SMT-lösare. Det vanligaste är SMT-LIB-standarden, som är baserad på S-uttryck (det vill säga samma som programmeringsspråket Lisp). Andra standardiserade format som ofta stöds är DIMACS-formatet som används av många booleska SAT-lösare och CVC-formatet som används av CVC-familjen av automatiska satsbevisare.

SMT-LIB-formatet kommer också med ett antal standardiserade prestandatester som används i en årlig tävling för SMT-lösare, SMT-COMP. Ursprungligen hölls tävlingen under Computer Aided Verification-konferensen (CAV), men numera hålls tävlingen som en del av SMT Workshop, som är ansluten till den internationella konferensen IJCAR.

Tillämpningar 
SMT-lösare används till formell verifiering av program och hårdvara, för programvarutestning baserat på symbolisk exekvering, och för programsyntes, i synnerhet generering av programfragment genom sökning över möjliga program. Utöver verifiering har SMT-lösare också använts för modellering av teoretiska scenarier, inklusive modellering av aktörers föreställningar i spelteorier för modellering av avtal för icke-spridning av kärnvapen.

Se även 

 Villkorsprogrammering

Referenser 

NP-kompletta problem
Datavetenskap
Kombinatorik
Logik