Kielégíthetőségi modulo elméletek forrásának megtekintése

Az [[Számítástudomány|informatikában]] és a [[Matematikai logika|matematikai logikában]] a '''SAT modulo elméletek''' (SMT) annak meghatározása, hogy egy matematikai formula kielégíthető-e. A [[Logikai kielégítési probléma|Boole-féle kielégíthetőségi problémát]] (SAT) általánosítja a [[Valós számok|valós számokat]], [[Egész számok|egész számokat]] és/vagy különböző [[Adatszerkezet|adatszerkezeteket]], például listákat, [[Tömb (adatszerkezet)|tömböket]], bitvektorokat és [[String|stringeket]] tartalmazó összetettebb formulákra. Az elnevezés onnan ered, hogy ezeket a kifejezéseket egy bizonyos [[Formális elmélet|formális elméleten]] belül („modulo”) értelmezik az [[Elsőrendű logika|elsőrendű logikában]] egyenlőséggel (gyakran a [[Kvantor (logika)|kvantorokat]] kizárva). 

Az SMT-megoldók olyan eszközök, amelyek célja az SMT-probléma megoldása a bemenetek egy gyakorlati részhalmazára. Az SMT-megoldókat, mint például a Z3 és a CVC4, a számítástechnika számos alkalmazási területének építőelemeként használják, többek között az [[Automatizált tételbizonyítás|automatizált tételbizonyításban]], a programelemzésben, a programellenőrzésben és a [[Fehérdobozos tesztelés|szoftvertesztelésben]].

Mivel a [[boolean]] kielégíthetőség már [[NP-teljesség|NP-teljes]], az SMT-probléma tipikusan NP-nehéz, és sok elmélet esetében eldönthetetlen. A kutatók azt vizsgálják, hogy mely elméletek vagy elméletek részhalmazai vezetnek eldönthető SMT-problémához és az eldönthető esetek számítási bonyolultságához. Az így kapott döntési eljárásokat gyakran közvetlenül SMT-megoldókban implementálják; lásd például a Presburger-aritmetika eldönthetőségét. Az SMT felfogható korlát-elégedettségi problémaként, és így a megszorítások programozásának bizonyos formalizált megközelítése.

== Alapvető terminológia ==
Formálisan szólva, egy SMT-példány egy olyan formula az [[Elsőrendű nyelv|elsőrendű logikában]], ahol néhány függvény- és predikátumszimbólumnak további értelmezései vannak, és az SMT az a probléma, hogy meghatározzuk, hogy egy ilyen formula kielégíthető-e. Más szóval, képzeljük el a [[Logikai kielégítési probléma|logikai kielégíthetőségi probléma]] (SAT) egy olyan példányát, amelyben a bináris változók egy részét nem bináris változók megfelelő halmaza feletti predikátumokkal helyettesítjük. A predikátum nem bináris változók bináris értékű függvénye. A példa predikátumok közé tartoznak a lineáris [[Egyenlőtlenség|egyenlőtlenségek]] (pl. <math>3x + 2y - z \geq 4</math>) vagy értelmezetlen kifejezéseket és funkciószimbólumokat tartalmazó egyenlőségek (pl. <math>f(f(u, v), v) = f(u, v)</math> ahol <math>f</math> két argumentum bizonyos nem meghatározott függvénye). Ezeket a predikátumokat a hozzájuk rendelt egyes elméletek szerint osztályozzák. Például a valós változók feletti lineáris egyenlőtlenségeket a lineáris valós aritmetika elméletének szabályai szerint értékeljük ki, míg az értelmezhetetlen kifejezéseket és függvényszimbólumokat tartalmazó predikátumokat az egyenlőséggel értelmezhetetlen függvények elméletének (néha üres elméletnek is nevezik) szabályai szerint értékeljük ki. További elméletek közé tartozik a tömbök és a listaszerkezetek elmélete (hasznos a [[Program (informatika)|számítógépes programok]] modellezéséhez és ellenőrzéséhez), valamint a bitvektorok elmélete (hasznos a hardvertervek modellezéséhez és ellenőrzéséhez). Alelméletek is lehetségesek: például a differencialogika a lineáris aritmetika egy részelmélete, amelyben minden egyenlőtlenség alakjára korlátozódik. <math>x - y > c</math> változókhoz <math>x</math> és <math>y</math> és állandó <math>c</math>.

A legtöbb SMT-megoldó csak a logikájuk [[Kvantor (logika)|kvantifikátormentes]] töredékeit támogatja.

== Kifejezőerő ==
Az SMT-példány a boolean SAT-példány ('''logikai kielégítési probléma''') általánosítása, amelyben a változók különböző halmazait a különböző mögöttes elméletekből származó predikátumok helyettesítik. Az SMT-formulák sokkal gazdagabb modellezési nyelvet biztosítanak, mint a boolean SAT-formulák. Például egy SMT-képlet lehetővé teszi, hogy egy mikroprocesszor adatútvonal-műveleteit nem bit-, hanem szószinten modellezzük.

Ehhez képest a válaszhalmaz-programozás szintén predikátumokon (pontosabban atomi formulákból alkotott atomi mondatokon) alapul. Az SMT-vel ellentétben a válaszhalmaz-programok nem rendelkeznek kvantorokkal, és nem tudják könnyen kifejezni az olyan megkötéseket, mint a lineáris aritmetika vagy a differencia-logika - az ASP legfeljebb olyan Boole-problémákhoz alkalmas, amelyek az értelmezhetetlen függvények szabad elméletére redukálódnak. A 32 bites egész számok bitvektorként való implementálása az ASP-ben ugyanazoktól a problémáktól szenved, amelyekkel a korai SMT-megoldók is szembesültek: Az olyan „nyilvánvaló” azonosságokat, mint <math>x+y=y+x</math>, nehéz levezetni.

A korlátozó logikai programozás támogatja a lineáris aritmetikai kényszereket, de egy teljesen más elméleti keretben. Az SMT-megoldókat kiterjesztették a magasabb rendű logikai formulák megoldására is.

== Megoldó megközelítések ==
Az SMT-példányok megoldására tett korai kísérletek közé tartozott, hogy lefordították őket boolean SAT-példányokká (pl. egy 32 bites egész szám változót 32 egybites változóval kódoltak, megfelelő súlyokkal, és a szószintű műveleteket, mint például a „plusz”, alacsonyabb szintű logikai műveletekkel helyettesítették a biteken), és ezt a képletet átadták egy boolean SAT-megoldónak. Ennek a megközelítésnek, amelyet eager megközelítésnek neveznek, megvannak az előnyei: az SMT-képletnek egy egyenértékű boolean SAT-képletté történő előfeldolgozásával a meglévő boolean SAT-megoldók „úgy, ahogy van” használhatók, és teljesítményük és kapacitásuk idővel javulhat. 

Másrészről viszont a mögöttes elméletek magas szintű szemantikájának elvesztése azt jelenti, hogy a boolean SAT-megoldónak a szükségesnél sokkal keményebben kell dolgoznia a „nyilvánvaló” tények felfedezéséhez (mint például a <math>x + y = y + x</math> az egész számok összeadására). Ez a megfigyelés számos SMT-megoldó kifejlesztéséhez vezetett, amelyek szorosan integrálják a DPLL-stílusú keresés logikai érvelését olyan elmélet-specifikus megoldókkal (T- solver), amelyek egy adott elmélet predikátumainak [[Konjunkció|konjunkcióit]] (AND-okat) kezelik. Ezt a megközelítést lusta megközelítésnek nevezik.

A DPLL(T) elnevezésű architektúra a boolean következtetés felelősségét a DPLL-alapú SAT-megoldóra bízza, amely viszont egy jól definiált interfészen keresztül lép kapcsolatba a T elmélet megoldójával. Az elmélet megoldójának csak az elméleti predikátumok SAT-megoldótól átadott kötőszavak megvalósíthatóságának ellenőrzésével kell foglalkoznia, miközben a formula boolean keresési terét vizsgálja. Ahhoz azonban, hogy ez az integráció jól működjön, az elméletmegoldónak képesnek kell lennie a propagációban és a konfliktuselemzésben való részvételre, azaz képesnek kell lennie arra, hogy a már megállapított tényekből új tényeket következtessen, valamint hogy tömör magyarázatot adjon a megvalósíthatatlanságra, ha elméleti konfliktusok merülnek fel. Más szóval, az elméletmegoldónak inkrementálisnak és [[Visszalépéses keresés|visszavezethetőnek]] kell lennie.

== SMT a megdönthetetlen elméletekhez ==
A legtöbb elterjedt SMT-megközelítés támogatja a megfejthető elméleteket. Számos valós világbeli rendszer azonban csak transzcendens függvényeket tartalmazó, a valós számok feletti nemlineáris aritmetikával modellezhető, például egy repülőgép és annak viselkedése. Ez a tény motiválja az SMT-probléma kiterjesztését a nemlineáris elméletekre, pl. annak meghatározására, hogy

: <math>
\begin{array}{lr}
& (\sin(x)^3 = \cos(\log(y)\cdot x) \vee b \vee -x^2 \geq 2.3y) \wedge \left(\neg b \vee y < -34.4 \vee \exp(x) > {y \over x}\right)
\end{array}
</math>

ahol

: <math>b \in {\mathbb B}, x,y \in {\mathbb R}</math>

kielégíthető. Ezután az ilyen problémák általában eldönthetetlenek lesznek. (A [[Valós zárt test|valós zárt testek]] elmélete, és így a valós számok teljes elsőrendű elmélete azonban eldönthető a kvantorelimináció segítségével. Ez [[Alfred Tarski|Alfred Tarskinak]] köszönhető). A természetes számok elsőrendű elmélete összeadással (de nem szorzással), az úgynevezett Presburger-aritmetika szintén eldönthető. Mivel a konstansokkal való szorzás megvalósítható egymásba ágyazott összeadásként, az aritmetika sok számítógépes programban kifejezhető Presburger-aritmetikával, ami eldönthető formulákat eredményez.

Valós számok feletti eldönthetetlen aritmetikai elméletekből származó elméleti atomok boolean kombinációit kezelő SMT-megoldókra példa az ABsolver, amely egy klasszikus DPLL(T) architektúrát alkalmaz egy nemlineáris optimalizációs csomaggal, mint (szükségszerűen hiányos) alárendelt elméleti megoldó, és az iSAT, amely a DPLL SAT-megoldás és az intervallumkorlátozás terjedésének egyesítésére, az iSAT algoritmusra épül.

<!--
== Megoldók ==
Az alábbi táblázat összefoglalja a számos elérhető SMT-megoldó néhány jellemzőjét. Az "SMT-LIB" oszlop az SMT-LIB nyelvvel való kompatibilitást jelzi; sok "igen" jelzésű rendszer csak az SMT-LIB régebbi verzióit támogatja, vagy csak részben támogatja a nyelvet. A "CVC" oszlop a CVC nyelv támogatását jelzi. A "DIMACS" oszlop a DIMACS formátum támogatását jelzi.

A projektek nem csak a funkciók és a teljesítmény tekintetében különböznek, hanem a környező közösség életképességében, a projekt iránti folyamatos érdeklődésében, valamint a dokumentáció, a javítások, a tesztek és a fejlesztések hozzájárulásának képességében is.

=== Szabványosítás és az SMT-COMP megoldóverseny ===
Több kísérlet is létezik az SMT-megoldók (és az automatizált tételbizonyítók, gyakran szinonimaként használt kifejezés) szabványosított interfészének leírására. A legjelentősebb az SMT-LIB szabvány, amely egy S-kifejezéseken alapuló nyelvet biztosít. Más, általánosan támogatott szabványosított formátumok a DIMACS formátum, amelyet számos boolean SAT-megoldó támogat, és a CVC formátum, amelyet a CVC automatizált tételbizonyító használ.


Az SMT-LIB formátumhoz számos szabványosított benchmark is tartozik, és lehetővé tette az SMT-COMP elnevezésű SMT-megoldók közötti éves versenyt. A verseny kezdetben a Computer Aided Verification (CAV) konferencia keretében zajlott, 2020-tól, azonban a verseny az SMT Workshop részeként kerül megrendezésre, amely az International Joint Conference on Automated Reasoning (IJCAR) konferenciához kapcsolódik.
-->

== Alkalmazások ==
Az SMT-megoldók egyaránt hasznosak verifikációhoz, a programok helyességének bizonyításához, szimbolikus végrehajtáson alapuló szoftverteszteléshez, szintézishez, programrészletek generálásához a lehetséges programok terében való kereséssel. A szoftverellenőrzésen kívül az SMT-megoldókat típuskövetkeztetésre és elméleti forgatókönyvek modellezésére is használják, beleértve a szereplők nukleáris fegyverek ellenőrzésével kapcsolatos hiedelmeinek modellezését is. 

=== Igazolás ===
A számítógépes programok számítógépes ellenőrzése gyakran SMT-megoldókat használ. Elterjedt technika az előfeltételek, utófeltételek, ciklusfeltételek és állítások SMT-képletekre fordítása annak megállapítására, hogy az összes tulajdonság érvényes-e.

A Z3 SMT-megoldóra számos verifikátor épül. A [https://www.microsoft.com/en-us/research/project/boogie-an-intermediate-verification-language/?from=http%3A%2F%2Fresearch.microsoft.com%2Fen-us%2Fprojects%2Fboogie%2F Boogie] egy köztes verifikációs nyelv, amely a Z3-at használja egyszerű imperatív programok automatikus ellenőrzésére. A VCC verifikátor a konkurens C nyelvhez a Boogie-t, valamint a [https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/?from=http%3A%2F%2Fresearch.microsoft.com%2Fen-us%2Fprojects%2Fdafny%2F Dafny]-t imperatív objektumalapú programokhoz, a [https://www.microsoft.com/en-us/research/project/chalice/?from=http%3A%2F%2Fresearch.microsoft.com%2Fen-us%2Fprojects%2Fchalice%2F Chalice]-t konkurens programokhoz és a [https://www.microsoft.com/en-us/research/project/spec/?from=http%3A%2F%2Fresearch.microsoft.com%2Fen-us%2Fprojects%2Fspecsharp%2F Spec#]-t a C# nyelvhez használja. Az F* egy függően tipizált nyelv, amely a Z3-at használja bizonyítások keresésére; a fordító ezeket a bizonyításokat végigviszi, hogy bizonyítást hordozó bájtkódot állítson elő. A [https://www.pm.inf.ethz.ch/research/viper.html Viper verifikációs infrastruktúra] a verifikációs feltételeket kódolja a Z3-ba. Az [https://hackage.haskell.org/package/sbv sbv] könyvtár a Haskell programok SMT-alapú verifikációját biztosítja, és a felhasználó számos megoldó közül választhat, mint például a Z3, ABC, Boolector, CVC4, MathSAT és Yices.

Az [http://alt-ergo.ocamlpro.com/ Alt-Ergo] SMT-megoldóra számos hitelesítő is épül. A felnőtt alkalmazások listája:

* [http://why3.lri.fr/ A Why3], a deduktív programellenőrzés platformja az Alt-Ergo-t használja fő próbájaként;
* CAVEAT, a CEA által kifejlesztett és az Airbus által használt C-ellenőrző; Az Alt-Ergo bekerült egyik legutóbbi repülőgépének DO-178C minősítésébe;
* A Frama-C, a C-kód elemzésére szolgáló keretrendszer az Alt-Ergo-t használja a Jessie és a WP beépülő modulokban (a "deduktív programellenőrzésnek" szentelve);
* A SPARK a CVC4-et és az Alt-Ergo-t (a GNATprove mögött) használja bizonyos állítások ellenőrzésének automatizálására a SPARK 2014-ben;
* Az Atelier-B használhatja az Alt-Ergo-t fő próbája helyett (a siker 84%-ról 98%-ra növeli az [http://alt-ergo.lri.fr/documents/ABZ-2014.pdf ANR Bware projekt benchmarkjait] {{Wayback|url=http://alt-ergo.lri.fr/documents/ABZ-2014.pdf |date=20141129015810 }});
* A Rodin, a Systerel által kifejlesztett B-metódus keretrendszer, az Alt-Ergo-t használhatja háttérként;
* [http://cubicle.lri.fr/ Cubicle], egy nyílt forráskódú modellellenőrző a tömb alapú átmeneti rendszerek biztonsági tulajdonságainak ellenőrzésére.
* [https://www.easycrypt.info/ EasyCrypt], egy eszközkészlet a valószínűségi számítások relációs tulajdonságaival kapcsolatos érveléshez ellentétes kóddal.

Sok SMT-megoldó megvalósítja az [http://smt-lib.org/ SMTLIB2] nevű közös interfészformátumot (az ilyen fájlok általában " <code>.smt2</code> " kiterjesztéssel rendelkeznek). A [https://ucsd-progsys.github.io/liquidhaskell-blog/ LiquidHaskell] eszköz egy finomítási típusú alapú ellenőrzőt valósít meg a Haskell számára, amely bármilyen SMTLIB2-kompatibilis megoldót használhat, pl. CVC4, MathSat vagy Z3.

=== Szimbolikus végrehajtás alapú elemzés és tesztelés ===
Az SMT-megoldók fontos alkalmazási területe a szimbolikus végrehajtás programok elemzésére és tesztelésére (pl. konkolikus tesztelés), különösen a biztonsági rések megtalálására. [idézet szükséges] Példaként említhetjük a Microsoft Research SAGE, a KLEE, az S2E és a Triton eszközeit. A szimbolikus végrehajtás alkalmazásaihoz használt SMT-megoldók közé tartozik a Z3, az STP Archiválva 2015-04-06 a Wayback Machine-ben, a [https://z3string.github.io/ Z3str megoldócsalád] és a Boolector. 

== Jegyzetek ==
{{jegyzetek}}

== Fordítás ==

* {{fordítás|en|Satisfiability modulo theories|oldid=1079196496}}

[[Kategória:Lapok ellenőrizetlen fordításokkal]]
[[Kategória:NP-teljes problémák]]
[[Kategória:Számítási bonyolultság]]