Problemet med tilfredsstillelse af formler i teorier

Den aktuelle version af siden er endnu ikke blevet gennemgået af erfarne bidragydere og kan afvige væsentligt fra den version , der blev gennemgået den 15. januar 2019; checks kræver 2 redigeringer .

Problemet med tilfredsstillelse af formler i teorier ( engelsk satisfiability modulo theories , SMT) er problemet med løselighed for logiske formler under hensyntagen til de teorier, der ligger til grund for dem. Eksempler på sådanne teorier for SMT-formler er: teorier om heltal og reelle tal, teorier om lister, arrays, bitvektorer osv.

Grundlæggende begreber

Formelt er en SMT-formel en formel i førsteordenslogik , hvor nogle funktioner og prædikatsymboler har en yderligere fortolkning. Opgaven er at afgøre, om den givne formel er gennemførlig. Med andre ord, i modsætning til tilfredshedsproblemet for booleske formler , indeholder SMT-formlen i stedet for boolske variabler vilkårlige variabler, og prædikaterne er boolske funktioner af disse variable.

Eksempler på prædikater er lineære uligheder ( ) eller ligheder, der involverer såkaldte ufortolkede termer eller funktionssymboler : , hvor er en udefineret funktion af to argumenter. Prædikater fortolkes efter den teori, de tilhører. For eksempel evalueres lineære uligheder over reelle variable efter reglerne i teorien om lineær reel aritmetik, mens prædikater over ufortolkede termer og funktionssymboler vurderes efter reglerne i teorien om ufortolkede funktioner med lighed (også kaldet tom teori) . SMT omfatter også array- og listeteorier (ofte brugt til programmodellering og verifikation ) og bitvektorteori (ofte brugt til hardwaremodellering og verifikation). Subteorier er også mulige: For eksempel er differenslogik en subteori af lineær aritmetik, hvor ulighederne er begrænset til følgende form for variablerne og konstanten . $3x+2y-z\geqslant 4$ $f(f(u,v),v)=f(u,v)$ $f$ $xy\leq c$ $x$ $y$ $c$

De fleste SMT - løsere understøtter kun ikke-kvantificerende formler .

SMT's udtrykskraft

SMT-formlen er en generalisering af den boolske SAT-formel , hvor variablerne er erstattet af prædikater fra de relevante teorier. Derfor giver SMT'er flere modelleringsmuligheder end SAT-formler. For eksempel giver SMT-formlen dig mulighed for at modellere operationerne af en funktion af mikroprocessormoduler på ordniveau snarere end på bitniveau .

SMT-løsere

De første forsøg på at løse SMT-problemer var rettet mod at konvertere dem til SAT-formler (for eksempel blev 32-bit variabler kodet med 32 boolske variable, der koder de tilsvarende operationer på ord til lavniveauoperationer på bit) og løse SAT-formlen med en løser. Denne tilgang har sine fordele - den giver dig mulighed for at bruge eksisterende SAT-løsere uden ændringer og bruge de optimeringer, der er foretaget i dem. På den anden side betyder tabet af højniveau-semantikken i de bagvedliggende teorier, at SAT-løseren skal gå meget langt for at udlede "oplagte" fakta (såsom til addition). Denne overvejelse har ført til specialiserede SMT-løsere, der integrerer konventionelle DPLL -stil booleske beviser med teorispecifikke løsere ( T-solvere ), der arbejder med disjunktioner og konjunktioner af prædikater fra en given teori. $x+y=y+x$

DPLL(T)-arkitekturen overfører de boolske bevisfunktioner til SAT-løseren, som igen interagerer med løseren af teorien T. SAT-løseren genererer modeller, hvor nogle af bogstaverne, der kommer ind uden negation, ikke er boolske variable, men atomudsagn af nogle, muligvis multi-sorterede, teori første orden. Teoriløseren forsøger at finde uoverensstemmelser i de modeller, der sendes til den, og hvis der ikke findes en sådan inkonsistens, er formlen erklæret tilfredsstillende. For at denne integration skal fungere, skal teoriløseren deltage i konfliktanalysen ved at give forklaringer på det umulige, når der opstår konflikter, som er lagret i løseren baseret på DPLL-arkitekturen. Da antallet af SAT-modeller er begrænset, vil opregning føre til et svar i begrænset tid [1] .

Understøttede og aktivt udviklede løsere: Alt-Ergo, Barcelogic, Beaver, Boolector, CVC3, DPT, MathSAT, OpenSMT, SatEEn, Spear, STP, UCLID, veriT, Yices, Z3.
Andre: Argo-lib, Ario, CVC, CVC Lite, Fx7, haRVey, HTP, ICS, LPSAT, RDL, Sammy, Simplify, Simplics, STeP, SVC, Tsat++.

Noter

↑ M. Armand, G. Faure, B. Gregoire, C. Keller, L. Thery, B. Werner. En modulær integration af SAT/SMT-løsere til Coq gennem 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. Løsning af SAT- og SAT-modulteorier: Fra en abstrakt Davis-Putnam-Logemann-Loveland-procedure til DPLL( T ) // Journal of the ACM. - 2006. - T. 53 , nr. 6 . - s. 937-977.
Biere, A. og Gomes, CP Theory and Applications of Satisfiability Testing - SAT 2006: 9th International Conference, Seattle, WA, USA, 12.-15. august 2006, Proceedings . — Springer, 2006. — S. 142-155 . — 438 s. — ISBN 9783540372066 .
D.Yurichev, Hurtig introduktion til SAT/SMT-løsere og symbolsk udførelse