Problemet med tillfredsställelse av formler i teorier

Den aktuella versionen av sidan har ännu inte granskats av erfarna bidragsgivare och kan skilja sig väsentligt från versionen som granskades den 15 januari 2019; kontroller kräver 2 redigeringar .

Problemet med tillfredsställelse av formler i teorier ( engelska satisfiability modulo theories , SMT) är problemet med lösbarhet för logiska formler, med hänsyn tagen till de teorier som ligger till grund för dem. Exempel på sådana teorier för SMT-formler är: teorier om heltal och reella tal, teorier om listor, matriser, bitvektorer , etc.

Grundläggande begrepp

Formellt är en SMT-formel en formel i första ordningens logik där vissa funktioner och predikatsymboler har en ytterligare tolkning. Uppgiften är att avgöra om den givna formeln är genomförbar. Med andra ord, till skillnad från tillfredsställbarhetsproblemet för booleska formler , i stället för booleska variabler, innehåller SMT-formeln godtyckliga variabler, och predikaten är booleska funktioner för dessa variabler.

Exempel på predikat är linjära olikheter ( ) eller likheter som involverar så kallade otolkade termer eller funktionssymboler : , där är någon odefinierad funktion av två argument. Predikat tolkas enligt den teori de tillhör. Till exempel utvärderas linjära olikheter över reella variabler enligt reglerna i teorin för linjär reell aritmetik, medan predikat över otolkade termer och funktionssymboler utvärderas enligt reglerna för teorin om otolkade funktioner med likhet (även kallad tom teori) . SMT inkluderar också array- och listteorier (används ofta för programmodellering och verifiering ) och bitvektorteori (används ofta för hårdvarumodellering och verifiering). Delteorier är också möjliga: till exempel är skillnadslogik en subteori för linjär aritmetik, där olikheterna är begränsade till följande form för variablerna och konstanten . $3x+2y-z\geqslant 4$ $f(f(u,v),v)=f(u,v)$ $f$ $xy\leq c$ $x$ $y$ $c$

De flesta SMT - lösare stöder endast formler som inte är kvantifierande .

Den uttrycksfulla kraften hos SMT

SMT-formeln är en generalisering av den booleska SAT-formeln där variablerna ersätts av predikat från relevanta teorier. Därför ger SMT:er fler modelleringsalternativ än SAT-formler. Till exempel låter SMT-formeln dig modellera operationerna för en funktion av mikroprocessormoduler på ordnivå snarare än på bitnivå .

SMT-lösare

De första försöken att lösa SMT-problem syftade till att konvertera dem till SAT-formler (till exempel kodades 32-bitarsvariabler med 32 booleska variabler som kodade motsvarande operationer på ord till lågnivåoperationer på bitar) och lösa SAT-formeln med en lösare. Detta tillvägagångssätt har sina fördelar - det låter dig använda befintliga SAT-lösare utan ändringar och använda de optimeringar som gjorts i dem. Å andra sidan innebär förlusten av semantiken på hög nivå i de underliggande teorierna att SAT-lösaren måste gå långt för att härleda "uppenbara" fakta (som för addition). Detta övervägande har lett till specialiserade SMT-lösare som integrerar konventionella DPLL -stil booleska bevis med teorispecifika lösare ( T-lösare ) som arbetar med disjunktioner och konjunktioner av predikat från en given teori. $x+y=y+x$

DPLL(T)-arkitekturen överför de booleska bevisfunktionerna till SAT-lösaren, som i sin tur interagerar med lösaren av teorin T. SAT-lösaren genererar modeller där några av de bokstavliga som kommer in utan negation inte är booleska variabler, utan atomära uttalanden av någon, möjligen mångsorterad, teori av första ordningen. Teorilösaren försöker hitta inkonsekvenser i de modeller som skickas till den, och om ingen sådan inkonsekvens hittas, förklaras formeln tillfredsställande. För att denna integration ska fungera måste teorilösaren delta i konfliktanalysen genom att ge förklaringar till omöjligheten när konflikter uppstår, vilka lagras i lösaren baserat på DPLL-arkitekturen. Eftersom antalet SAT-modeller är ändligt kommer uppräkningen att leda till ett svar i ändlig tid [1] .

Stöds och aktivt utvecklade lösare: Alt-Ergo, Barcelogic, Beaver, Boolector, CVC3, DPT, MathSAT, OpenSMT, SatEEn, Spear, STP, UCLID, veriT, Yices, Z3.
Övriga: Argo-lib, Ario, CVC, CVC Lite, Fx7, haRVey, HTP, ICS, LPSAT, RDL, Sammy, Simplify, Simplics, STeP, SVC, Tsat++.

Anteckningar

↑ M. Armand, G. Faure, B. Gregoire, C. Keller, L. Thery, B. Werner. En modulär integration av SAT/SMT-lösare till Coq genom Proof Witnesses First International Conference, CPP 2011, Kenting, Taiwan, 7-9 december 2011. Proceedings. DOI 10.1007/978-3-642-25379-9_12

Litteratur

Nieuwenhuis, R.; Oliveras, A.; Tinelli, C. Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL( T ) // Journal of the ACM. - 2006. - T. 53 , nr 6 . - s. 937-977.
Biere, A. och Gomes, CP Theory and Applications of Satisfiability Testing - SAT 2006: 9th International Conference, Seattle, WA, USA, 12-15 augusti 2006, Proceedings . — Springer, 2006. — S. 142-155 . — 438 sid. — ISBN 9783540372066 .
D.Yurichev, Snabb introduktion till SAT/SMT-lösare och symbolisk utförande