Kielégíthetőségi modulo elméletek

Az informatikában és a matematikai logikában a SAT modulo elméletek (SMT) annak meghatározása, hogy egy matematikai formula kielégíthető-e. A Boole-féle kielégíthetőségi problémát (SAT) általánosítja a valós számokat, egész számokat és/vagy különböző adatszerkezeteket, például listákat, tömböket, bitvektorokat és stringeket tartalmazó összetettebb formulákra. Az elnevezés onnan ered, hogy ezeket a kifejezéseket egy bizonyos formális elméleten belül („modulo”) értelmezik az elsőrendű logikában egyenlőséggel (gyakran a 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ásban, a programelemzésben, a programellenőrzésben és a szoftvertesztelésben.

Mivel a boolean kielégíthetőség már 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[szerkesztés]

Formálisan szólva, egy SMT-példány egy olyan formula az 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í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égek (pl. $3x+2y-z\geq 4$ ) vagy értelmezetlen kifejezéseket és funkciószimbólumokat tartalmazó egyenlőségek (pl. $f(f(u,v),v)=f(u,v)$ ahol $f$ 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 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. $x-y>c$ változókhoz $x$ és $y$ és állandó $c$ .

A legtöbb SMT-megoldó csak a logikájuk kvantifikátormentes töredékeit támogatja.

Kifejezőerő[szerkesztés]

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 $x+y=y+x$ , 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[szerkesztés]

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 $x+y=y+x$ 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ó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 visszavezethetőnek kell lennie.

SMT a megdönthetetlen elméletekhez[szerkesztés]

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

{\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}}

ahol

b\in {\mathbb {B} },x,y\in {\mathbb {R} }

kielégíthető. Ezután az ilyen problémák általában eldönthetetlenek lesznek. (A 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 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.

Alkalmazások[szerkesztés]

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[szerkeszté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 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 Dafny-t imperatív objektumalapú programokhoz, a Chalice-t konkurens programokhoz és a 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 Viper verifikációs infrastruktúra a verifikációs feltételeket kódolja a Z3-ba. Az 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 Alt-Ergo SMT-megoldóra számos hitelesítő is épül. A felnőtt alkalmazások listája:

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 ANR Bware projekt benchmarkjait);
A Rodin, a Systerel által kifejlesztett B-metódus keretrendszer, az Alt-Ergo-t használhatja háttérként;
Cubicle, egy nyílt forráskódú modellellenőrző a tömb alapú átmeneti rendszerek biztonsági tulajdonságainak ellenőrzésére.
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 SMTLIB2 nevű közös interfészformátumot (az ilyen fájlok általában " .smt2 " kiterjesztéssel rendelkeznek). A 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[szerkeszté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 Z3str megoldócsalád és a Boolector.

Jegyzetek[szerkesztés]

Fordítás[szerkesztés]

Ez a szócikk részben vagy egészben a Satisfiability modulo theories című angol Wikipédia-szócikk ezen változatának fordításán alapul. Az eredeti cikk szerkesztőit annak laptörténete sorolja fel. Ez a jelzés csupán a megfogalmazás eredetét és a szerzői jogokat jelzi, nem szolgál a cikkben szereplő információk forrásmegjelöléseként.