Problém splnitelnosti formulí v teoriích

Aktuální verze stránky ještě nebyla zkontrolována zkušenými přispěvateli a může se výrazně lišit od verze recenzované 15. ledna 2019; kontroly vyžadují 2 úpravy .

Problém splnitelnosti formulí v teoriích ( anglicky  satisfiability modulo theories , SMT) je problémem řešitelnosti logických formulí s přihlédnutím k teoriím, na nichž jsou založeny. Příklady takových teorií pro vzorce SMT jsou: teorie celých a reálných čísel, teorie seznamů, polí, bitových vektorů atd.

Základní pojmy

Formálně je vzorec SMT vzorec  v logice prvního řádu, ve kterém mají některé funkce a predikátové symboly další výklad. Úkolem je zjistit, zda je daný vzorec proveditelný. Jinými slovy, na rozdíl od problému splnitelnosti pro booleovské vzorce , namísto booleovských proměnných obsahuje vzorec SMT libovolné proměnné a predikáty jsou booleovské funkce těchto proměnných.

Příklady predikátů jsou lineární nerovnosti ( ) nebo rovnosti zahrnující tzv. neinterpretované členy nebo funkční symboly : , kde je nějaká nedefinovaná funkce dvou argumentů. Predikáty se vykládají podle teorie, ke které patří. Například lineární nerovnosti nad reálnými proměnnými jsou hodnoceny podle pravidel teorie lineární reálné aritmetiky, zatímco predikáty nad neinterpretovanými pojmy a funkčními symboly jsou hodnoceny podle pravidel teorie neinterpretovaných funkcí s rovností (také nazývané teorie prázdné) . SMT také zahrnuje teorie polí a seznamů (často používané pro modelování a ověřování programů ) a teorii bitových vektorů (často používané pro modelování a ověřování hardwaru). Možné jsou také podteorie: například diferenční logika  je podteorií lineární aritmetiky, ve které jsou nerovnosti omezeny na následující formu pro proměnné a a konstantu .

Většina SMT řešitelů podporuje pouze nekvantifikátorové vzorce . 

Výrazová síla SMT

Vzorec SMT je zobecněním vzorce Boolean SAT , ve kterém jsou proměnné nahrazeny predikáty z příslušných teorií. Proto SMT poskytují více možností modelování než vzorce SAT. Vzorec SMT vám například umožňuje modelovat operace funkce mikroprocesorových modulů na úrovni slova , nikoli na úrovni bitů .

Řešiče SMT

První pokusy o řešení problémů SMT směřovaly k jejich převedení na vzorce SAT (například 32bitové proměnné byly zakódovány pomocí 32 booleovských proměnných kódujících odpovídající operace se slovy do nízkoúrovňových operací na bitech) a řešení vzorce SAT pomocí řešitel. Tento přístup má své výhody – umožňuje používat stávající SAT řešiče beze změn a využívat v nich provedené optimalizace. Na druhou stranu ztráta sémantiky na vysoké úrovni základních teorií znamená, že řešitel SAT musí jít do značné míry, aby odvodil „zřejmá“ fakta (například pro sčítání). Tato úvaha vedla ke specializovaným řešičům SMT, které integrují konvenční booleovské důkazy ve stylu DPLL s řešiče specifickými pro teorii ( T-solvery ), které pracují s disjunkcemi a konjunkcemi predikátů z dané teorie.

Architektura DPLL(T) přenáší booleovské důkazové funkce do SAT řešiče, který zase interaguje s řešičem teorie T. SAT řešič generuje modely, ve kterých některé literály vstupující bez negace nejsou booleovské proměnné, ale atomické příkazy nějaké, možná vícetříděné, teorie prvního řádu. Řešitel teorie se snaží najít nekonzistence v modelech, které mu byly předány, a pokud žádná taková nekonzistence není nalezena, vzorec je prohlášen za splnitelný. Aby tato integrace fungovala, musí se řešitel teorií podílet na analýze konfliktů poskytnutím  vysvětlení neproveditelnosti, když dojde ke konfliktům, která jsou uložena v řešiči založeném na architektuře DPLL. Protože počet modelů SAT je konečný, výčet povede k odpovědi v konečném čase [1] .

Poznámky

  1. ↑ M. Armand, G. Faure, B. Gregoire, C. Keller, L. Thery, B. Werner. Modulární integrace SAT/SMT řešitelů do Coq prostřednictvím první mezinárodní konference důkazních svědků, CPP 2011, Kenting, Tchaj-wan, 7.–9. prosince 2011. Sborník příspěvků. DOI 10.1007/978-3-642-25379-9_12

Literatura

Odkazy