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 ( $x=1\land y=2\cdot x$ ). 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 redigera

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. $3x+2y-z\geq 4$ ) eller likheter som inbegriper otolkade termer och funktionssymboler, t.ex. $f(f(u,v),v)=f(u,v)$ där $f$ ä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.^[1]

Lösare redigera

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 redigera

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),^[2]^[3] men numera hålls tävlingen som en del av SMT Workshop, som är ansluten till den internationella konferensen IJCAR.^[4]

Tillämpningar redigera

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.^[5]

Se även redigera

Villkorsprogrammering

Referenser redigera

^ Bultan, Tevfik (2017) (på engelska). String Analysis for Software Verification and Security. Springer International Publishing. doi:10.1007/978-3-319-68670-7. ISBN 978-3-319-68668-4. http://link.springer.com/10.1007/978-3-319-68670-7. Läst 20 oktober 2020
^ (på engelska) SMT-COMP: Satisfiability Modulo Theories Competition. https://link.springer.com/chapter/10.1007%2F11513988_4.
^ (på engelska) The SMT-LIB Initiative and the Rise of SMT. https://link.springer.com/chapter/10.1007%2F978-3-642-19583-9_2.
^ ”SMT-COMP 2020” (på amerikansk engelska). SMT-COMP. https://smt-comp.github.io/2020/.
^ Beaumont, Paul; Evans, Neil; Huth, Michael; Plant, Tom (2015). Pernul, Günther; Y A Ryan, Peter; Weippl, Edgar. red. ”Confidence Analysis for Nuclear Arms Control: SMT Abstractions of Bayesian Belief Networks” (på engelska). Computer Security -- ESORICS 2015. Lecture Notes in Computer Science (Cham: Springer International Publishing): sid. 521–540. doi:10.1007/978-3-319-24174-6_27. ISBN 978-3-319-24174-6. https://link.springer.com/chapter/10.1007%2F978-3-319-24174-6_27.

[1] Bultan, Tevfik (2017) (på engelska). String Analysis for Software Verification and Security. Springer International Publishing. doi:10.1007/978-3-319-68670-7. ISBN 978-3-319-68668-4. http://link.springer.com/10.1007/978-3-319-68670-7. Läst 20 oktober 2020

[2] (på engelska) SMT-COMP: Satisfiability Modulo Theories Competition. https://link.springer.com/chapter/10.1007%2F11513988_4.

[3] (på engelska) The SMT-LIB Initiative and the Rise of SMT. https://link.springer.com/chapter/10.1007%2F978-3-642-19583-9_2.

[4] ”SMT-COMP 2020” (på amerikansk engelska). SMT-COMP. https://smt-comp.github.io/2020/.

[5] Beaumont, Paul; Evans, Neil; Huth, Michael; Plant, Tom (2015). Pernul, Günther; Y A Ryan, Peter; Weippl, Edgar. red. ”Confidence Analysis for Nuclear Arms Control: SMT Abstractions of Bayesian Belief Networks” (på engelska). Computer Security -- ESORICS 2015. Lecture Notes in Computer Science (Cham: Springer International Publishing): sid. 521–540. doi:10.1007/978-3-319-24174-6_27. ISBN 978-3-319-24174-6. https://link.springer.com/chapter/10.1007%2F978-3-319-24174-6_27.

[1]

[2]

[3]

[4]

[5]